Axe
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.
Subtopics
- R1cs-verification-with-axe
- Verifying an R1CS using the Axe toolkit.
- Prove-equal-with-axe
- Prove that two items (DAGs or terms) are equivalent for all values of all of their variables.
- Dags
- Axe's DAG data structure
- Stp
- An SMT solver used by the Axe toolkit
- Lifters
- Axe Lifters
- Read-jar
- Read in a .jar file and parse and register classes for use by Axe.
- Read-class
- Read in a .class file and parse and register the class for use by Axe.
