GACAL

GACAL verifies C programs by exploring execution traces to identify conjectured invariants and applying the ACL2s theorem prover to establish program correctness.

Key Features:

• Invariant Search: Systematically searches execution traces of C programs to identify candidate invariants.
• Theorem Proving with ACL2s: Uses the ACL2s theorem prover to formally verify candidate invariants.
• Iterative Verification Process: Performs iterative discovery and verification, beginning with simpler invariants and progressively addressing more complex ones.
• Integration with External Tools: Connects to external tools via the interface provided by ACL2s to extend verification capabilities.

Scientific Applications:

• C Program Verification: Verifying correctness and detecting logical errors in C programs through invariant-based proofs.
• Bioinformatics Algorithm Validation: Validating correctness and reliability of computational algorithms used in bioinformatics.

Methodology:

Explores the space of possible invariants using traces from the input C program; identifies candidate invariants; employs the ACL2s theorem prover via its interface to verify invariants; iterates from simpler to more complex invariants.