4 papers
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…
Verification Modulo Tested Library Contracts
Abhishek Uppar, Omar Muhammad, Sumanth Prabhu +3
We consider the problem of verification modulo tested library contracts as a step towards automating the verification of client programs that use complex libraries. We formulate th…
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…
Synthesizing DSLs for Few-Shot Learning
Paul Krogmeier, P. Madhusudan
We study the problem of synthesizing domain-specific languages (DSLs) for few-shot learning in symbolic domains. Given a base language and instances of few-shot learning problems,…