Benjamin Delaware

43 papers A* 5A 2B 3C 1Journal 28Unranked 4

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	Adaptive Proof Refinement with LLM-Guided Strategy Selection. CoRR Minghai Lu, Zhe Zhou, Danning Xie, Songlin Jia, Benjamin Delaware, Tianyi Zhang
2025	J	`jnl`	From Traces to Program Incorrectness: A Type-Theoretic Approach. CoRR Yongwei Yuan, Zhe Zhou, Julia Belyakova, Benjamin Delaware, Suresh Jagannathan
2025	J	`jnl`	KestRel: Relational Verification using E-Graphs for Program Alignment. Proc. ACM Program. Lang. Robert Dickerson, Prasita Mukherjee, Benjamin Delaware
2025	A*	`conf`	LLM-Assisted Synthesis of High-Assurance C Programs. ASE Prasita Mukherjee, Minghai Lu, Benjamin Delaware
2025	J	`jnl`	Type-Based Incorrectness Reasoning. CoRR Zhe Zhou, Benjamin Delaware, Suresh Jagannathan
2025	J	`jnl`	We've Got You Covered: Type-Guided Repair of Incomplete Input Generators. CoRR Patrick LaFontaine, Zhe Zhou, Ashish Mishra, Suresh Jagannathan, Benjamin Delaware
2025	J	`jnl`	We've Got You Covered: Type-Guided Repair of Incomplete Input Generators. Proc. ACM Program. Lang. Patrick LaFontaine, Zhe Zhou, Ashish Mishra, Suresh Jagannathan, Benjamin Delaware
2024	J	`jnl`	A HAT Trick: Automatically Verifying Representation Invariants Using Symbolic Finite Automata. CoRR Zhe Zhou, Qianchuan Ye, Benjamin Delaware, Suresh Jagannathan
2024	J	`jnl`	A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata. Proc. ACM Program. Lang. Zhe Zhou, Qianchuan Ye, Benjamin Delaware, Suresh Jagannathan
2024	J	`jnl`	KestRel: Relational Verification Using E-Graphs for Program Alignment. CoRR Robert Dickerson, Prasita Mukherjee, Benjamin Delaware
2024	A*	`conf`	Proof Automation with Large Language Models. ASE Minghai Lu, Benjamin Delaware, Tianyi Zhang
2024	J	`jnl`	Proof Automation with Large Language Models. CoRR Minghai Lu, Benjamin Delaware, Tianyi Zhang
2024	J	`jnl`	Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation. Proc. ACM Program. Lang. Qianchuan Ye, Benjamin Delaware
2024	J	`jnl`	Towards Automated Verification of LLM-Synthesized C Programs. CoRR Prasita Mukherjee, Benjamin Delaware
2023	J	`jnl`	A Type-Based Approach to Divide-and-Conquer Recursion in Coq. Proc. ACM Program. Lang. Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins, J. Garrett Morris, Aaron Stump
2023	J	`jnl`	Covering All the Bases: Type-Based Verification of Test Input Generators. CoRR Zhe Zhou, Ashish Mishra, Benjamin Delaware, Suresh Jagannathan
2023	J	`jnl`	Covering All the Bases: Type-Based Verification of Test Input Generators. Proc. ACM Program. Lang. Zhe Zhou, Ashish Mishra, Benjamin Delaware, Suresh Jagannathan
2023	J	`jnl`	Taype: A Policy-Agnostic Language for Oblivious Computation. Proc. ACM Program. Lang. Qianchuan Ye, Benjamin Delaware
2023	J	`jnl`	Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation. CoRR Qianchuan Ye, Benjamin Delaware
2022	J	`jnl`	Oblivious algebraic data types. Proc. ACM Program. Lang. Qianchuan Ye, Benjamin Delaware
2022	B	`conf`	RHLE: Modular Deductive Verification of Relational ∀ ∃ Properties. APLAS Robert Dickerson, Qianchuan Ye, Michael K. Zhang, Benjamin Delaware
2021	J	`jnl`	Data-Driven Abductive Inference of Library Specifications. CoRR Zhe Zhou, Robert Dickerson, Benjamin Delaware, Suresh Jagannathan
2021	J	`jnl`	Data-driven abductive inference of library specifications. Proc. ACM Program. Lang. Zhe Zhou, Robert Dickerson, Benjamin Delaware, Suresh Jagannathan
2021	B	`conf`	HACCLE: metaprogramming for secure multi-party computation. GPCE Yuyan Bao, Kirshanthan Sundararajah, Raghav Malik, Qianchuan Ye, Christopher Wagner, Nouraldin Jaber, Fei Wang, Mohammad Hassan Ameri, Donghang Lu, Alexander Seto, Benjamin Delaware, Roopsha Samanta, Aniket Kate, Christina Garman, Jeremiah Blocki, Pierre-David Letourneau, Benoît Meister, Jonathan Springer, Tiark Rompf, Milind Kulkarni
2021	J	`jnl`	Relational Type Theory (All Proofs). CoRR Aaron Stump, Benjamin Delaware, Christopher Jenkins
2021	J	`jnl`	Repairing Serializability Bugs in Distributed Database Programs via Automated Schema Refactoring. CoRR Kia Rahmani, Kartik Nagar, Benjamin Delaware, Suresh Jagannathan
2021	A*	`conf`	Repairing serializability bugs in distributed database programs via automated schema refactoring. PLDI Kia Rahmani, Kartik Nagar, Benjamin Delaware, Suresh Jagannathan
2020	—	`conf`	Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. IJCAR (2) Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala
2020	J	`jnl`	HACCLE: An Ecosystem for Building Secure Multi-Party Computations. CoRR Yuyan Bao, Kirshanthan Sundararajah, Raghav Malik, Qianchuan Ye, Christopher Wagner, Fei Wang, Mohammad Hassan Ameri, Donghang Lu, Alexander Seto, Benjamin Delaware, Roopsha Samanta, Aniket Kate, Christina Garman, Jeremiah Blocki, Pierre-David Letourneau, Benoît Meister, Jonathan Springer, Tiark Rompf, Milind Kulkarni
2020	J	`jnl`	RHLE: Automatic Verification of ∀∃-Hyperproperties. CoRR Robert Dickerson, Qianchuan Ye, Benjamin Delaware
2019	B	`conf`	A verified protocol buffer compiler. CPP Qianchuan Ye, Benjamin Delaware
2019	J	`jnl`	CLOTHO: Directed Test Generation for Weakly Consistent Database Systems. CoRR Kia Rahmani, Kartik Nagar, Benjamin Delaware, Suresh Jagannathan
2019	J	`jnl`	CLOTHO: directed test generation for weakly consistent database systems. Proc. ACM Program. Lang. Kia Rahmani, Kartik Nagar, Benjamin Delaware, Suresh Jagannathan
2019	J	`jnl`	Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. Proc. ACM Program. Lang. Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, Adam Chlipala
2018	J	`jnl`	Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats. CoRR Sorawit Suriyakarn, Clément Pit-Claudel, Benjamin Delaware, Adam Chlipala
2017	—	`conf`	The End of History? Using a Proof Assistant to Replace Language Design with Library Design. SNAPL Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, Katherine Ye
2017	C	`conf`	Using Coq to write fast and correct Haskell. Haskell John Wiegley, Benjamin Delaware
2015	A*	`conf`	Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. POPL Benjamin Delaware, Clément Pit-Claudel, Jason Gross, Adam Chlipala
2013	A*	`conf`	Meta-theory à la carte. POPL Benjamin Delaware, Bruno C. d. S. Oliveira, Tom Schrijvers
2013	A	`conf`	Modular monadic meta-theory. ICFP Benjamin Delaware, Steven Keuchel, Tom Schrijvers, Bruno C. d. S. Oliveira
2011	A	`conf`	Product lines of theorems. OOPSLA Benjamin Delaware, William R. Cook, Don S. Batory
2009	—	`conf`	A machine-checked model of safe composition. FOAL Benjamin Delaware, William R. Cook, Don S. Batory
2009	—	`conf`	Fitting the pieces together: a machine-checked model of safe composition. ESEC/SIGSOFT FSE Benjamin Delaware, William R. Cook, Don S. Batory