KestRel at OOPSLA 2025
Our work on KestRel will appear at OOPSLA 2025.
KestRel at the 2023 E-Graphs Workshop
I presented some ongoing work on KestRel at the 2023 E-Graphs workshop at PLDI this year. KestRel is an e-graph based approach for aligning programs for relational verification. An e-graph is saturated with rewrite rules over an algebra of alignments, and desirable alignments are extracted using traditional e-graph techniques combined with a novel data-driven approach.
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.