Panagiotis (Pete) Manolios
College of Computer and Information Science
Northeastern University

GACAL: Conjecture-Based Verification

Benjamin Quiring and Panagiotis Manolios.
TACAS, 2020 © Springer


GACAL verifies C programs by searching over the space of possible invariants, using traces of the input program to identify potential invariants. GACAL uses the ACL2s theorem prover to verify these potential invariants, using an interface provided by ACL2s for connecting with external tools. GACAL iteratively searches for and proves invariants of increasing complexity until the program is verified.

PDF (389K) © Springer