ACL2 (“A Computational Logic for Applicative Common Lisp”) is an interactive theorem prover based on first order logic.
Papers related to ACL2 theorem prover
- Abstract stobjs and their application to ISA modeling [goel:acl2:2013]
- Simulation and formal verification of x86 machine-code programs that make system calls [goel:fmcad:2014]
- Engineering a formal, executable x86 ISA simulator for software verification [goel:pcs:2017]
- Formal verification of application and system programs based on a validated x86 ISA model [goel:phd:2016]
- A robust machine code proof framework for highly secure applications [hardin:acl2:2006]
- An industrial strength theorem prover for a logic based on Common Lisp [kaufmann:ieeetse:1997]