A verified protocol buffer compiler. - Qianchuan Ye; Benjamin Delaware (CPP, 2019)

Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. - Benjamin Delaware; Sorawit Suriyakarn; Clément Pit-Claudel; Qianchuan Ye; Adam Chlipala (Proc. ACM Program. Lang., 2019)

RHLE: Automatic Verification of ∀∃-Hyperproperties. - Robert Dickerson; Qianchuan Ye; Benjamin Delaware (CoRR, 2020)

HACCLE: An Ecosystem for Building Secure Multi-Party Computations. - Yuyan Bao; Kirshanthan Sundararajah; Raghav Malik; Qianchuan Ye; Christopher Wagner; Fei Wang 046; Mohammad Hassan Ameri; Donghang Lu; Alexander Seto; Benjamin Delaware; Roopsha Samanta; Aniket Kate; et al. (CoRR, 2020)

HACCLE: metaprogramming for secure multi-party computation. - Yuyan Bao; Kirshanthan Sundararajah; Raghav Malik; Qianchuan Ye; Christopher Wagner; Nouraldin Jaber; Fei Wang 046; Mohammad Hassan Ameri; Donghang Lu; Alexander Seto; Benjamin Delaware; Roopsha Samanta; et al. (GPCE, 2021)

RHLE: Modular Deductive Verification of Relational ∀ ∃ Properties. - Robert Dickerson; Qianchuan Ye; Michael K. Zhang; Benjamin Delaware (APLAS, 2022)

Oblivious algebraic data types. - Qianchuan Ye; Benjamin Delaware (Proc. ACM Program. Lang., 2022)

Taype: A Policy-Agnostic Language for Oblivious Computation. - Qianchuan Ye; Benjamin Delaware (Proc. ACM Program. Lang., 2023)

Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation. - Qianchuan Ye; Benjamin Delaware (Proc. ACM Program. Lang., 2024)

A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata. - Zhe Zhou; Qianchuan Ye; Benjamin Delaware; Suresh Jagannathan (Proc. ACM Program. Lang., 2024)