4 papers · 1 filter
Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale
Muhammad A. A. Pirzada, Julian Parsert, Weiqi Wang +2
Loop invariant synthesis remains a central and pivotal bottleneck in formal software verification. Recent LLM-based Neuro-Symbolic tools have achieved impressive solve rates. Howev…
ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification
Pierre Dantas, Lucas Cordeiro, Waldir Junior
The Efficient SMT-Based Context-Bounded Model Checker (ESBMC) has grown from a research prototype for verifying embedded ANSI-C software into one of the most versatile and industri…
ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification
Muhammad A. A. Pirzada, Weiqi Wang, Yiannis Charalambous +2
Formal verification of large C programs is impeded by state-space explosion: Bounded Model Checking (BMC) tools must encode the entire state space up to the predetermined bound by…
UnitTenX: Generating Tests for Legacy Packages with AI Agents Powered by Formal Verification
Yiannis Charalambous, Claudionor N. Coelho, Luis Lamb +1
This paper introduces UnitTenX, a state-of-the-art open-source AI multi-agent system designed to generate unit tests for legacy code, enhancing test coverage and critical value tes…