PV2 GACALgenerates increasingly stronger invariants for an external prover

GACAL verifies C programs by searching over the space of possible invariants, using traces of the input program to identify potential invariants.

Application domain/field

Expected input

Format:

Internals

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.

Comments

License: GNU GPLv3

Links

Last commit date

16 January 2020

Related papers

https://doi.org/10.1007/978-3-030-45237-7_26 (TACAS '20)

Last publication date

17 April 2020

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.