The Axe toolkit
The Axe toolkit provides a variety of tools for software verification, including lifters-into-logic, rewriters, theorem provers, and equivalence checkers.
Most of Axe is now available in the ACL2 Community books, under kestrel/axe/, though much work remains to document it.
See the Axe webpage for more information.
- Verifying an R1CS using the Axe toolkit.
- Axe's DAG data structure
- An SMT solver used by the Axe toolkit
- Axe Lifters
- Read in a .jar file and parse and register classes for use by Axe.
- Read in a .class file and parse and register the class for use by Axe.