arXiv.itsnick.co

an independent field guide to 23 million papers from arXiv & OpenAlex — not affiliated with arXiv.org

Author

Benjamin Delaware

43 papers · 2009–2026

2009: 62010: 02011: 22012: 02013: 42014: 12015: 12016: 02017: 22018: 12019: 32020: 22021: 42022: 12023: 62024: 42025: 42026: 2
2009peak 6 in 20092026

Frequent co-authors

Papers

showing 1–25 of 43 RSS

Fiat

Benjamin Delaware, Clément Pit-Claudel, Jason Gross +1 more

Artificial Intelligence · · cited 87× · DOI ↗ · more like this ·

We present Fiat, a library for the Coq proof assistant supporting refinement of declarative specifications into efficient functional programs with a high degree of automation. Each refinement process leaves a proof trail, checkable by the normal Coq kernel, justifying its soundness. We focus on the synthesis of abstract data types that package methods with private data. We demonstrate the utility of our framework by applying it to the synthesis of query structures -- abstract data types with SQL-like query and insert operations. Fiat includes a library for writing specifications of query structures in SQL-inspired notation, expressing operations over relations (tables) in terms of mathematical sets. This library includes a suite of tactics for automating the refinement of specifications into efficient, correct-by-construction OCaml code. Using these tactics, a programmer can generate…

Product lines of theorems

Benjamin Delaware, William R. Cook, Don Batory

Artificial Intelligence · · cited 77× · DOI ↗ · more like this ·

Mechanized proof assistants are powerful verification tools, but proof development can be difficult and time-consuming. When verifying a family of related programs, the effort can be reduced by proof reuse. In this paper, we show how to engineer product lines with theorems and proofs built from feature modules. Each module contains proof fragments which are composed together to build a complete proof of correctness for each product. We consider a product line of programming languages, where each variant includes metatheory proofs verifying the correctness of its semantic definitions. This approach has been realized in the Coq proof assistant, with the proofs of each feature independently certifiable by Coq. These proofs are composed for each language variant, with Coq mechanically verifying that the composite proofs are correct. As validation, we formalize a core calculus for Java in…

Fitting the pieces together

Benjamin Delaware, William R. Cook, Don Batory

Artificial Intelligence · · cited 68× · DOI ↗ · more like this ·

Programs of a software product line can be synthesized by composing features which implement a unit of program functionality. In most product lines, only some combination of features are meaningful; feature models express the high-level domain constraints that govern feature compatibility. Product line developers also face the problem of safe composition - whether every product allowed by a feature model is type-safe when compiled and run. To study the problem of safe composition, we present Lightweight Feature Java (LFJ), an extension of Lightweight Java with support for features. We define a constraint-based type system for LFJ and prove its soundness using a full formalization of LFJ in Coq. In LFJ, soundness means that any composition of features that satisfies the typing constraints will generate a well-formed LJ program. If the constraints of a feature model imply these typing…

Modular monadic meta-theory

Benjamin Delaware, Steven Keuchel, Tom Schrijvers +1 more

Artificial Intelligence · The HKU Scholars Hub (University of Hong Kong) · · cited 36× · DOI ↗ · more like this ·

This paper presents 3MT, a framework for modular mechanized meta-theory of languages with effects. Using 3MT, individual language features and their corresponding definitions -- semantic functions, theorem statements and proofs-- can be built separately and then reused to create different languages with fully mechanized meta-theory. 3MT combines modular datatypes and monads to define denotational semantics with effects on a per-feature basis, without fixing the particular set of effects or language constructs.

A machine-checked model of safe composition

Benjamin Delaware, William R. Cook, Don Batory

Artificial Intelligence · · cited 36× · DOI ↗ · more like this ·

Programs of a software product line can be synthesized by composing features which implement some unit of program functionality. In most product lines, only some combination of features are meaningful; feature models express the high-level domain constraints that govern feature compatibility. Product line developers also face the problem of safe composition -- whether every product allowed by a feature model is type-safe when compiled and run. To study the problem of safe composition, we present Lightweight Feature Java (LFJ), an extension of Lightweight Java with support for features. We define a constraint-based type system for LFJ and prove its soundness using a full formalization of LFJ in Coq. In LFJ, soundness means that any composition of features that satisfies the typing constraints will generate a well-formed LJ program. If the constraints of a feature model imply these typing…

Narcissus: correct-by-construction derivation of decoders and encoders from binary formats

Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel +2 more

Artificial Intelligence · Proceedings of the ACM on Programming Languages · · cited 25× · DOI ↗ · more like this ·

It is a neat result from functional programming that libraries of parser combinators can support rapid construction of decoders for quite a range of formats. With a little more work, the same combinator program can denote both a decoder and an encoder. Unfortunately, the real world is full of gnarly formats, as with the packet formats that make up the standard Internet protocol stack. Most past parser-combinator approaches cannot handle these formats, and the few exceptions require redundancy – one part of the natural grammar needs to be hand-translated into hints in multiple parts of a parser program. We show how to recover very natural and nonredundant format specifications, covering all popular network packet formats and generating both decoders and encoders automatically. The catch is that we use the Coq proof assistant to derive both kinds of artifacts using tactics, automatically…

The End of History? Using a Proof Assistant to Replace Language Design with Library Design

Adam Chlipala, Benjamin Delaware, Samuel Duchovni +5 more

Information Systems · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · · cited 12× · DOI ↗ · more like this ·

Functionality of software systems has exploded in part because of advances in programming-language support for packaging reusable functionality as libraries. Developers benefit from the uniformity that comes of exposing many interfaces in the same language, as opposed to stringing together hodgepodges of command-line tools. Domain-specific languages may be viewed as an evolution of the power of reusable interfaces, when those interfaces become so flexible as to deserve to be called programming languages. However, common approaches to domain-specific languages give up many of the hard-won advantages of library-building in a rich common language, and even the traditional approach poses significant challenges in learning new APIs. We suggest that instead of continuing to develop new domain-specific languages, our community should embrace library-based ecosystems within very expressive…

A verified protocol buffer compiler

Qianchuan Ye, Benjamin Delaware

Computer Networks and Communications · · cited 11× · DOI ↗ · more like this ·

The code responsible for serializing and deserializing untrusted external data is a vital component of any software that communicates with the outside world, as any bugs in these components can compromise the entire system. This is particularly true for verified systems which rely on trusted code to process external data, as any defects in the parsing code can invalidate any formal proofs about the system. One way to reduce the trusted code base of these systems is to use interface generators like Protocol Buffer and ASN.1 to generate serializers and deserializers from data descriptors. Of course, these generators are not immune to bugs.

Proof Automation with Large Language Models

Minghai Lu, Benjamin Delaware, Tianyi Zhang

cs.SE · · cited 9× · arXiv ↗ · more like this ·

Interactive theorem provers such as Coq are powerful tools to formally guarantee the correctness of software. However, using these tools requires significant manual effort and expertise. While Large Language Models (LLMs) have shown promise in automatically generating informal proofs in natural language, they are less effective at generating formal proofs in interactive theorem provers. In this paper, we conduct a formative study to identify common mistakes made by LLMs when asked to generate formal proofs. By analyzing 520 proof generation errors made by GPT-3.5, we found that GPT-3.5 often identified the correct high-level structure of a proof, but struggled to get the lower-level details correct. Based on this insight, we propose PALM, a novel generate-then-repair approach that first prompts an LLM to generate an initial proof and then leverages targeted symbolic methods to…

Oblivious algebraic data types

Qianchuan Ye, Benjamin Delaware

Artificial Intelligence · Proceedings of the ACM on Programming Languages · · cited 8× · DOI ↗ · more like this ·

Secure computation allows multiple parties to compute joint functions over private data without leaking any sensitive data, typically using powerful cryptographic techniques. Writing secure applications using these techniques directly can be challenging, resulting in the development of several programming languages and compilers that aim to make secure computation accessible. Unfortunately, many of these languages either lack or have limited support for rich recursive data structures, like trees. In this paper, we propose a novel representation of structured data types, which we call oblivious algebraic data types, and a language for writing secure computations using them. This language combines dependent types with constructs for oblivious computation, and provides a security-type system which ensures that adversaries can learn nothing more than the result of a computation. Using this…

Covering All the Bases: Type-Based Verification of Test Input Generators

Z. Zhou, Ashish Mishra, Benjamin Delaware +1 more

Software · Proceedings of the ACM on Programming Languages · · cited 7× · DOI ↗ · more like this ·

Test input generators are an important part of property-based testing (PBT) frameworks. Because PBT is intended to test deep semantic and structural properties of a program, the outputs produced by these generators can be complex data structures, constrained to satisfy properties the developer believes is most relevant to testing the function of interest. An important feature expected of these generators is that they be capable of producing all acceptable elements that satisfy the function’s input type and generator-provided constraints. However, it is not readily apparent how we might validate whether a particular generator’s output satisfies this coverage requirement. Typically, developers must rely on manual inspection and post-mortem analysis of test runs to determine if the generator is providing sufficient coverage; these approaches are error-prone and difficult to scale as…

HACCLE: metaprogramming for secure multi-party computation

Yuyan Bao, Kirshanthan Sundararajah, Raghav Malik +9 more

Artificial Intelligence · · cited 6× · DOI ↗ · more like this ·

Cryptographic techniques have the potential to enable distrusting parties to collaborate in fundamentally new ways, but their practical implementation poses numerous challenges. An important class of such cryptographic techniques is known as Secure Multi-Party Computation (MPC). Developing Secure MPC applications in realistic scenarios requires extensive knowledge spanning multiple areas of cryptography and systems. And while the steps to arrive at a solution for a particular application are often straightforward, it remains difficult to make the implementation efficient, and tedious to apply those same steps to a slightly different application from scratch. Hence, it is an important problem to design platforms for implementing Secure MPC applications with minimum effort and using techniques accessible to non-experts in cryptography.

Meta-theory à la carte

Benjamin Delaware, Bruno C. d. S. Oliveira, Tom Schrijvers

Artificial Intelligence · ACM SIGPLAN Notices · · cited 6× · DOI ↗ · more like this ·

Formalizing meta-theory, or proofs about programming languages, in a proof assistant has many well-known benefits. Unfortunately, the considerable effort involved in mechanizing proofs has prevented it from becoming standard practice. This cost can be amortized by reusing as much of existing mechanized formalizations as possible when building a new language or extending an existing one. One important challenge in achieving reuse is that the inductive definitions and proofs used in these formalizations are closed to extension. This forces language designers to cut and paste existing definitions and proofs in an ad-hoc manner and to expend considerable effort to patch up the results. The key contribution of this paper is the development of an induction technique for extensible Church encodings using a novel reinterpretation of the universal property of folds. These encodings provide the…

A HAT Trick: Automatically Verifying Representation Invariants Using Symbolic Finite Automata

Zhe Zhou, Qianchuan Ye, Benjamin Delaware +1 more

cs.PL · · cited 5× · arXiv ↗ · more like this ·

Functional programs typically interact with stateful libraries that hide state behind typed abstractions. One particularly important class of applications are data structure implementations that rely on such libraries to provide a level of efficiency and scalability that may be otherwise difficult to achieve. However, because the specifications of the methods provided by these libraries are necessarily general and rarely specialized to the needs of any specific client, any required application-level invariants must often be expressed in terms of additional constraints on the (often) opaque state maintained by the library. In this paper, we consider the specification and verification of such representation invariants using symbolic finite automata (SFA). We show that SFAs can be used to succinctly and precisely capture fine-grained temporal and data-dependent histories of interactions…

Taype: A Policy-Agnostic Language for Oblivious Computation

Qianchuan Ye, Benjamin Delaware

Artificial Intelligence · Proceedings of the ACM on Programming Languages · · cited 4× · DOI ↗ · more like this ·

Secure multiparty computation (MPC) allows for joint computation over private data from multiple entities, usually backed by powerful cryptographic techniques that protect sensitive data. Several high-level programming languages have been proposed to make writing MPC applications accessible to non-experts. These languages typically require developers to enforce security policies within the logic of the secure application itself, making it difficult to update security requirements, or to experiment with different policies. This paper presents the design and implementation of Taype, a language that permits security concerns to be decoupled from the program logic. To do so, Taype provides the first implementation of oblivious algebraic data types and tape semantics, two language features recently proposed by a core calculus for oblivious computation, λ OADT + . We evaluate our…

Repairing Serializability Bugs in Distributed Database Programs via Automated Schema Refactoring

Kia Rahmani, Kartik Nagar, Benjamin Delaware +1 more

cs.PL · · cited 4× · arXiv ↗ · more like this ·

Serializability is a well-understood concurrency control mechanism that eases reasoning about highly-concurrent database programs. Unfortunately, enforcing serializability has a high-performance cost, especially on geographically distributed database clusters. Consequently, many databases allow programmers to choose when a transaction must be executed under serializability, with the expectation that transactions would only be so marked when necessary to avoid serious concurrency bugs. However, this is a significant burden to impose on developers, requiring them to (a) reason about subtle concurrent interactions among potentially interfering transactions, (b) determine when such interactions would violate desired invariants, and (c) then identify the minimum number of transactions whose executions should be serialized to prevent these violations. To mitigate this burden, in this paper we…

Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats

Benjamin Delaware, Sorawit Suriyakarn, Clément Pit--Claudel +2 more

cs.PL · · cited 3× · arXiv ↗ · more like this ·

It is a neat result from functional programming that libraries of parser combinators can support rapid construction of decoders for quite a range of formats. With a little more work, the same combinator program can denote both a decoder and an encoder. Unfortunately, the real world is full of gnarly formats, as with the packet formats that make up the standard Internet protocol stack. Most past parser-combinator approaches cannot handle these formats, and the few exceptions require redundancy -- one part of the natural grammar needs to be hand-translated into hints in multiple parts of a parser program. We show how to recover very natural and nonredundant format specifications, covering all popular network packet formats and generating both decoders and encoders automatically. The catch is that we use the Coq proof assistant to derive both kinds of artifacts using tactics…

KestRel: Relational Verification Using E-Graphs for Program Alignment

Robert Dickerson, Prasita Mukherjee, Benjamin Delaware

cs.PL · · cited 2× · arXiv ↗ · more like this ·

Many interesting program properties involve the execution of multiple programs, including observational equivalence, noninterference, co-termination, monotonicity, and idempotency. One strategy for verifying such relational properties is to construct and reason about an intermediate program whose correctness implies that the individual programs exhibit those properties. A key challenge in building an intermediate program is finding a good alignment of the original programs. An alignment puts subparts of the original programs into correspondence so that their similarities can be exploited in order to simplify verification. We propose an approach to intermediate program construction that uses e-graphs, equality saturation, and algebraic realignment rules to efficiently represent and build programs amenable to automated verification. A key ingredient of our solution is a novel data-driven…

Using Coq to write fast and correct Haskell

John Wiegley, Benjamin Delaware

Artificial Intelligence · · cited 2× · DOI ↗ · more like this ·

Correctness and performance are often at odds in the field of systems engineering, either because correct programs are too costly to write or impractical to execute, or because well-performing code involves so many tricks of the trade that formal analysis is unable to isolate the main properties of the algorithm.

Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant

Benjamin Delaware, Jason Gross, Adam Chlipala

Artificial Intelligence · DSpace@MIT (Massachusetts Institute of Technology) · · cited 2× · OpenAlex ↗ · more like this ·

We present Fiat, a library for the Coq proof assistant supporting refinement of declarative specifications into efficient functional programs with a high degree of automation. Each refinement process leaves a proof trail, checkable by the normal Coq kernel, justifying its soundness. We focus on the synthesis of abstract data types that package methods with private data. We demonstrate the utility of our framework by applying it to the synthesis of query structures – abstract data types with SQL-like query and insert operations. Fiat includes a library for writing specifications of query structures in SQL-inspired notation, expressing operations over relations (tables) in terms of mathematical sets. This library includes a set of tactics for automating the refinement of these specifications into efficient, correct-by-construction OCaml code. Using these tactics, a programmer can generate…

Trace-Guided Synthesis of Effectful Test Generators

Zhe Zhou, Ankush Desai, Benjamin Delaware +1 more

cs.PL · · cited 1× · arXiv ↗ · more like this ·

Several recently proposed program logics have incorporated notions of underapproximation into their design, enabling them to reason about reachability rather than safety. In this paper, we explore how similar ideas can be integrated into an expressive type and effect system. We use the resulting underapproximate type specifications to guide the synthesis of test generators that probe the behavior of effectful black-box systems. A key novelty of our type language is its ability to capture underapproximate behaviors of effectful operations using symbolic traces that expose latent data and control dependencies, constraints that must be preserved by the test sequences the generator outputs. We implement this approach in a tool called Clouseau, and evaluate it on a diverse range of applications by integrating Clouseau's synthesized generators into property-based testing frameworks like…

We've Got You Covered: Type-Guided Repair of Incomplete Input Generators

Patrick LaFontaine, Zhe Zhou, Ashish Mishra +2 more

cs.PL · · cited 1× · arXiv ↗ · more like this ·

Property-based testing (PBT) is a popular technique for automatically testing semantic properties of a program, specified as a pair of pre- and post-conditions. The efficacy of this approach depends on being able to quickly generate inputs that meet the precondition, in order to maximize the set of program behaviors that are probed. For semantically rich preconditions, purely random generation is unlikely to produce many valid inputs; when this occurs, users are forced to manually write their own specialized input generators. One common problem with handwritten generators is that they may be incomplete, i.e., they are unable to generate some values meeting the target precondition. This paper presents a novel program repair technique that patches an incomplete generator so that its range includes every valid input. Our approach uses a novel enumerative synthesis algorithm that leverages…

Towards Automated Verification of LLM-Synthesized C Programs

Prasita Mukherjee, Benjamin Delaware

cs.PL · · cited 1× · arXiv ↗ · more like this ·

We present \synver{}, a novel synthesis and verification framework for C programs, that deploys a Large Language Model (LLM) to search for a candidate program that satisfies the given specification. Our key idea is to impose syntactic and semantic biases on programs generated by LLMs, such that the synthesized program is more amenable to automated verification. Based on this idea, we propose a novel specification-verification tool, built on top of Verified Software Toolchain, that help automate the process. Our experiments on a diverse set of benchmarks drawn from the deductive program synthesis community, shows that this approach is scalable and extensible. The benchmarks constitute of specifications comprising of basic coding examples, Separation Logic based assertions, and API specifications.

Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation

Qianchuan Ye, Benjamin Delaware

cs.PL · · cited 1× · arXiv ↗ · more like this ·

Secure multiparty computation (MPC) techniques enable multiple parties to compute joint functions over their private data without sharing that data with other parties, typically by employing powerful cryptographic protocols to protect individual's data. One challenge when writing such functions is that most MPC languages force users to intermix programmatic and privacy concerns in a single application, making it difficult to change or audit a program's underlying privacy policy. Prior policy-agnostic MPC languages relied on dynamic enforcement to decouple privacy requirements from program logic. Unfortunately, the resulting overhead makes it difficult to scale MPC applications that manipulate structured data. This work proposes to eliminate this overhead by instead transforming programs into semantically equivalent versions that statically enforce user-provided privacy policies. We have…

PLDI2023 Artifact: Covering All the Bases: Type-Based Verification of Test Input Generators

Z. Zhou, Ashish Mishra, Benjamin Delaware +1 more

Hardware and Architecture · Zenodo (CERN European Organization for Nuclear Research) · · cited 1× · DOI ↗ · more like this ·

This artifact contains: README.md : the artifact guide. poirot-full.pdf: full paper with the appendix. poirot_pldi-2023.tar.gz: the docker image (optional, we recommend to pull from the docker hub, see README.md). Dockerfile: the docker file that can reproduce the docker image (optional, we recommend to pull from the docker hub, see README.md).