ACL2 is a software system consisting of a programming language, an extensible theory in a first-order logic, and an automated theorem prover. ACL2 is designed to support automated reasoning in inductive logical theories, mostly for software and hardware verification. The input language and implementation of ACL2 are written in Common Lisp. ACL2 is free and open-source software. Wikipedia

Created Year: 1990
Designed by: Robert S. Boyer
Developed by: Matt Kaufmann
Operating systems: Unix-like operating system

Wikidata: Q4650692

Programming paradigms: functional programming