11 citations · 33 across the 14 of their papers we have counts for
5 papers · 1 filter
Complete first-order reasoning for functional programs
Adithya Murali, Lucas Peña, Ranjit Jhala +1
Several practical tools for automatically verifying functional programs (e.g., Liquid Haskell and Leon for Scala programs) rely on a heuristic based on unrolling recursive function…
FO-Complete Program Verification for Heap Logics
Adithya Murali, Hrishikesh Balakrishnan, Aaron Councilman +1
We develop the first two heap logics that have implicit heaplets and that admit FO-complete program verification. The notion of FO-completeness is a theoretical guarantee that all…
Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
Neta Elad, Adithya Murali, Sharon Shoham
For over two decades Separation Logic has been arguably the most popular framework for reasoning about heap-manipulating programs, as well as reasoning about shared resources and p…
Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints
Adithya Murali, Lucas Peña, Eion Blanchard +2
Recursively defined linked data structures embedded in a pointer-based heap and their properties are naturally expressed in pure first-order logic with least fixpoint definitions (…
A First-Order Logic with Frames
Adithya Murali, Lucas Peña, Christof Löding +1
We propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using a construct Sp(.) that captures the implicit supports of formul…