February 6, 2025
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 given specification. Our key idea is to impose syntactic biases on programs generated by LLMs, such that the synthesized program is more amenable to automated verification. Based on this idea, we propose an ltac, on top of Verified Software Toolchain, that help automate the process. ur experiments on a diverse set of benchmarks drawn from the deductive program synthesis community, shows that this approach is feasible and extensible. The benchmarks constitute of specifications comprising of arrays, heap manipulating programs (lists and trees), and API calls.
About Prasita Mukherjee
Prasita Mukherjee is a PhD student working with Prof. Ben Delaware. Her research interest is in verification and neurosymbolic reasoning.