Preprints
Publications
-
Predictable Verification using Intrinsic Definitions
PLDI 2024
ACM Europe Best Paper Award -
Complete First-Order Reasoning for Properties of Functional Programs
OOPSLA 2023
This work will be presented as a tutorial at POPL 2024! -
A First Order Logic with Frames
TOPLAS 2023 -
Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints
OOPSLA 2022 -
Synthesizing Axiomatizations using Logic Learning
OOPSLA 2022 -
Composing Neural Learning and Symbolic Reasoning with an Application to Visual Discrimination
IJCAI-ECAI 2022
Explore our website of puzzles! -
Decidable Synthesis of Programs with Uninterpreted Functions
CAV 2020 -
A First Order Logic with Frames
ESOP 2020 Slides (with notes) -
Deciding Memory Safety for Single-Pass Heap-Manipulating Programs
POPL 2020 -
Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity
FMCAD 2019