Program
Verification
Book

PV6 ⊧ ACL2: A Computational Logic for Applicative Common Lispa full-fledged language to write specs and prove their properties

Logic and programming language which you can use to model computer systems, and a tool to help you prove properties of those models. i.e. theorem prover

Application domain/field

Theorem prover
Rewriting
Interactive theorem prover

Type of tool

Framework/Theorem prover

Comments

License: BSD-3

Links

Project page: https://www.cs.utexas.edu/users/moore/acl2/
Repository: https://github.com/acl2/acl2
- Last commit date: 03 Dec 2022 (default branch)
- Last commit date: 03 Dec 2022 (last activity)
Related repository, seems to be where the ACL2 system authors develop ACL2: https://github.com/acl2-devel/acl2-devel
- Last commit date: 20 Jul 2022 (default branch)
Try ACL2 online: https://new.proofpad.org/

Related papers

Rough Diamond: An Extension of Equivalence-Based Rewriting (ITP '14)
Rewriting with Equivalence Relations in ACL2 (Journal of Automated Reasoning '08)
ACL2 theorems about commercial microprocessors (FMCAD '96)
ACL2: an industrial strength version of Nqthm (COMPASS '96)
See also: https://www.cs.utexas.edu/users/moore/publications/acl2-papers.html

Last publication date

2014

ProVerB specific

Markdown description: view/edit
Contained in the ProVerB22 dataset (paper + artefact)

ProVerB is a part of SLEBoK. Last updated: February 2023.