3 papers
cs.PL2024
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.PL2024
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.…
cs.LO2023
OCTAL: Graph Representation Learning for LTL Model Checking
Prasita Mukherjee, Haoteng Yin
Model Checking is widely applied in verifying the correctness of complex and concurrent systems against a specification. Pure symbolic approaches while popular, suffer from the sta…