2 papers
cs.PL2025
Towards Automated Verification of LLM-Synthesized C Programs
Prasita Mukherjee, Benjamin Delaware
We present \synver{}, a novel synthesis and verification framework for C programs, that deploys a Large Language Model (LLM) to search for a candidate program that satisfies the gi…
cs.PL2025
KestRel: Relational Verification Using E-Graphs for Program Alignment
Robert Dickerson, Prasita Mukherjee, Benjamin Delaware
Many interesting program properties involve the execution of multiple programs, including observational equivalence, noninterference, co-termination, monotonicity, and idempotency.…