About

Ben Hardekopf is an Associate Professor of Computer Science at the University of California, Santa Barbara. He leads the Programming Languages Research Laboratory at UCSB, where his work focuses on the development and analysis of programming languages. His academic role involves teaching foundational courses in computer science, contributing to the education of students in this field. As a faculty member at UCSB's College of Creative Studies, he is engaged in advancing research in programming languages and related areas, supporting the university's mission to foster innovative and rigorous scientific inquiry.

Research topics

• Computer Science
• Computer Security
• Programming language
• Computer hardware
• Artificial Intelligence
• Embedded system
• Parallel computing
• Computer architecture

Selected publications

• Breccia: A Functional DSL Compiled to Egglog for Test Input Generation

  Lecture notes in computer science · 2026-01-01

  book-chapterSenior author
  PublisherDOI

• Control Logic Synthesis: Drawing the Rest of the OWL

  2024-04-27 · 2 citations

  articleOpen access

  System-on-chip (SoC) design requires complex reasoning about the interactions between an architectural specification, the microarchitectural datapath (e.g., functional units), and the control logic (which coordinates the datapath) to facilitate the critical computing tasks on which we all depend. Hardware specialization is now the expectation rather than the exception, meaning we need new hardware design tools to bring ideas to reality with both agility and correctness.

  PublisherOA PDFDOI

• Loop Rerolling for Hardware Decompilation

  Proceedings of the ACM on Programming Languages · 2023 · 9 citations

  Senior authorCorresponding
  • Computer Science
  • Computer Science
  • Programming language

  We introduce the new problem of hardware decompilation . Analogous to software decompilation, hardware decompilation is about analyzing a low-level artifact—in this case a netlist , i.e., a graph of wires and logical gates representing a digital circuit—in order to recover higher-level programming abstractions, and using those abstractions to generate code written in a hardware description language (HDL). The overall problem of hardware decompilation requires a number of pieces. In this paper we focus on one specific piece of the puzzle: a technique we call hardware loop rerolling . Hardware loop rerolling leverages clone detection and program synthesis techniques to identify repeated logic in netlists (such as would be synthesized from loops in the original HDL code) and reroll them into syntactic loops in the recovered HDL code. We evaluate hardware loop rerolling for hardware decompilation over a set of hardware design benchmarks written in the PyRTL HDL and industry standard SystemVerilog. Our implementation identifies and rerolls loops in 52 out of 53 of the netlists in our benchmark suite, and we show three examples of how hardware decompilation can provide concrete benefits: transpilation between HDLs, faster simulation times over netlists (with mean speedup of 6x), and artifact compaction (39% smaller on average).

  PublisherOA PDFDOI

• Aliasing Limits on Translating C to Safe Rust

  Proceedings of the ACM on Programming Languages · 2023 · 21 citations

  Senior authorCorresponding
  • Computer Science
  • Computer Science
  • Programming language

  The Rust language was created to provide safe low-level systems programming. There is both industrial and academic interest in the problem of (semi-)automatically translating C code to Rust in order to exploit Rust's safety guarantees. We study the effectiveness and limitations of existing techniques for automatically translating unsafe raw pointers (in Rust programs translated from C) into safe Rust references via ownership and lifetime inference. Our novel evaluation methodology enables our study to extend beyond prior studies, and to discover new information contradicting the conclusions of prior studies. We find that existing translation methods are severely limited by a lack of precision in the Rust compiler's safety checker, causing many safe pointer manipulations to be labeled as potentially unsafe. Leveraging this information, we propose methods for improving translation, based on encoding the results of a more precise analysis in a manner that is understandable to an unmodified Rust compiler. We implement one of our proposed methods, increasing the number of pointers that can be translated to safe Rust references by 75% over the baseline (from 12% to 21% of all pointers).

  PublisherOA PDFDOI

• PyLSE: a pulse-transfer level language for superconductor electronics

  2022-06-02 · 4 citations

  articleOpen accessSenior author

  Superconductor electronics (SCE) run at hundreds of GHz and consume only a fraction of the dynamic power of CMOS, but are naturally pulse-based, and operate on impulses with picosecond widths. The transiency of these operations necessitates using logic cells that are inherently stateful. Adopting stateful gates, however, implies an entire reconstruction of the design, simulation, and verification stack. Though challenging, this unique opportunity allows us to build a design framework from the ground up using fundamental principles of programming language design. To this end, we propose PyLSE, an embedded pulse-transfer level language for superconductor electronics. We define PyLSE through formal semantics based on transition systems, and build a framework around them to simulate and analyze SCE cells digitally. To demonstrate its features, we verify its results by model checking in UPPAAL, and compare its complexity and timing against a set of cells designed as analog circuit schematics and simulated in Cadence.

  PublisherOA PDFDOI

• Translating C to safer Rust

  Proceedings of the ACM on Programming Languages · 2021 · 46 citations

  Senior authorCorresponding
  • Computer Science
  • Computer Science
  • Computer Security

  Rust is a relatively new programming language that targets efficient and safe systems-level applications. It includes a sophisticated type system that allows for provable memory- and thread-safety, and is explicitly designed to take the place of unsafe languages such as C and C++ in the coding ecosystem. There is a large existing C and C++ codebase (many of which have been affected by bugs and security vulnerabilities due to unsafety) that would benefit from being rewritten in Rust to remove an entire class of potential bugs. However, porting these applications to Rust manually is a daunting task. In this paper we investigate the problem of automatically translating C programs into safer Rust programs--that is, Rust programs that improve on the safety guarantees of the original C programs. We conduct an in-depth study into the underlying causes of unsafety in translated programs and the relative impact of fixing each cause. We also describe a novel technique for automatically removing a particular cause of unsafety and evaluate its effectiveness and impact. This paper presents the first empirical study of unsafety in translated Rust programs (as opposed to programs originally written in Rust) and also the first technique for automatically removing causes of unsafety in translated Rust programs.

  PublisherOA PDFDOI

• Wire sorts: a language abstraction for safe hardware composition

  2021 · 12 citations

  Senior authorCorresponding
  • Computer Science
  • Computer Science
  • Programming language

  Effective digital hardware design fundamentally requires decomposing a design into a set of interconnected modules, each a distinct unit of computation and state. However, naively connecting hardware modules leads to real-world pathological cases which are surprisingly far from obvious when looking at the interfaces alone and which are very difficult to debug after synthesis. We show for the first time that it is possible to soundly abstract even complex combinational dependencies of arbitrary hardware modules through the assignment of IO ports to one of four new sorts which we call: to-sync, to-port, from-sync, and from-port. This new taxonomy, and the reasoning it enables, facilitates modularity by escalating problematic aspects of module input/output interaction to the language-level interface specification. We formalize and prove the soundness of our new wire sorts, implement them in a practical hardware description language, and demonstrate they can be applied and even inferred automatically at scale. Through an examination of the BaseJump STL, the OpenPiton manycore research platform, and a complete RISC-V implementation, we find that even on our biggest design containing 1.5 million primitive gates, analysis takes less than 31 seconds; that across 172 unique modules analyzed, the inferred sorts are widely distributed across our taxonomy; and that by using wire sorts, our tool is 2.6–33.9x faster at finding loops than standard synthesis-time cycle detection.

  PublisherOA PDFDOI

• Safe functional systems through integrity types and verified assembly

  Theoretical Computer Science · 2020-09-23

  articleOpen accessSenior author

  Building a trustworthy life-critical embedded system requires deep reasoning about the potential effects that sequences of machine instructions can have on full system operation. Rather than trying to analyze complete binaries and the countless ways their instructions can interact with one another — memory, side effects, control registers, implicit state, etc. — we explore a new approach. We propose an architecture controlled by a thin computational layer designed to tightly correspond with the lambda calculus, drawing on principles of functional programming to bring the assembly much closer to myriad reasoning frameworks, such as the Coq proof assistant. This approach allows assembly-level verified versions of critical code to operate safely in tandem with arbitrary code, including imperative and unverified system components, without the need for large supporting trusted computing bases. We demonstrate that this computational layer can be built in such a way as to simultaneously provide full programmability and compact, precise, and complete semantics, while still using hardware resources comparable to normal embedded systems. To demonstrate the practicality of this approach, our FPGA-implemented prototype runs an embedded medical application which monitors and treats life-threatening arrhythmias. Though the system integrates untrusted and imperative components, our architecture allows for the formal verification of multiple properties of the end-to-end system. We present a proof of correctness of the assembly-level implementation of the core algorithm in Coq, the integrity of trusted data via a non-interference proof, and a guarantee that our prototype meets critical timing requirements.

  PublisherDOI

• A Practical, Principled Measure of Fuzzer Appeal: A Preliminary Study

  2020-12-01 · 4 citations

  articleSenior author

  Fuzzers are important bug-finding tools in both academia and industry. To ensure scientific progress, we need a metric for fuzzer comparison. Bug-based metrics are impractical because (1) the definition of "bug" is vague, and (2) mapping bug-revealing inputs to bugs requires extensive domain knowledge.In this paper, we propose an automated method for comparing fuzzers that alleviates these problems. We replace the question "What bugs can this fuzzer find?" with "What changes in program behavior over time can this fuzzer detect?". Intuitively, fuzzers which find more behavioral changes are likely to find more bugs. However, unlike bugs, behavioral changes are well-defined and readily detectable. Our evaluation, executed on three targets with several fuzzers, shows that our method is consistent with bug-based metrics, but without associated difficulties. While further evaluation is needed to establish superiority, our results show that our method warrants further investigation.

  PublisherDOI

• Structural and Nominal Cross-Language Clone Detection

  Lecture notes in computer science · 2019-01-01 · 12 citations

  book-chapterOpen accessSenior author

  In this paper we address the challenge of cross-language clone detection. Due to the rise of cross-language libraries and applications (e.g., apps written for both Android and iPhone), it has become common for code fragments in one language to be ported over into another language in an extension of the usual “copy and paste” coding methodology. As with single-language clones, it is important to be able to detect these cross-language clones. However there are many real-world cross-language clones that existing techniques cannot detect. We describe the first general, cross-language algorithm that combines both structural and nominal similarity to find syntactic clones, thereby enabling more complete clone detection than any existing technique. This algorithm also performs comparably to the state of the art in single-language clone detection when applied to single-language source code; thus it generalizes the state of the art in clone detection to detect both single- and cross-language clones using one technique.

  PublisherOA PDFDOI

Recent grants

• SHF: Small: Static Analysis for Safe Browser Addons

  NSF · $500k · 2013–2018

• CAREER: Static Analysis for Dynamic Languages

  NSF · $513k · 2014–2019

Frequent coauthors

• Timothy Sherwood

  University of California, Santa Barbara

  20 shared

• Vineeth Kashyap

  GrammaTech (United States)

  17 shared

• Kyle Dewey

  California State University, Northridge

  13 shared

• Xun Li

  13 shared

• Lawton Nichols

  11 shared

• Jared Roesch

  11 shared

• Mohit Tiwari

  10 shared

• Frederic T. Chong

  University of Chicago

  10 shared