RHLE: Modular Deductive Verification of Relational ∀∃ Properties
A program logic for proving relational properties with liveness components I developed with Qianchuan Ye, Michael Zhang, and Ben Delaware appeared at APLAS 2022.
Data-Driven Abductive Inference of Library Specifications
Work with Zhe Zhou, Ben Delaware, and Suresh Jagannathan on inferring library specifications by black-box sampling of client behavior appeared at OOPSLA 2021. The accompanying artifact, Elrond, won a distinguished artifact award.
PurPL Seminar: Relational Reasoning with Specifications
I presented some ongoing work on relational verification with specified functions at Purdue’s weekly PurPL seminar. The talk is available on the PurPL website.
Smoother Signatures in Square's Android Client
A writeup I did for Square’s engineering blog describing techniques for improving the visual style and rendering performance of signatures in Square’s Android client.
SICP Scheme Interpreter in Haskell
The Scheme interpreter from Structure and Interpretation of Computer Programs by Abelson and Sussman, but written in Haskell.