ACL2 theorem prover

ACL2 theorem prover
[Google Scholar] [Website] [Wikipedia]

ACL2 (“A Computational Logic for Applicative Common Lisp”) is an interactive theorem prover based on first order logic.

  • 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]