ACL2 Sedan

The ACL2 Sedan theorem prover (ACL2s) is an Eclipse plug-in that provides a modern IDE, supports several modes of interaction, provides a powerful termination analysis engine, includes a rich support for "types" and seamlessly integrates semi-automated bug-finding methods with interactive theorem proving.

Application domain/field

Theorem proving

Type of tool

Theorem prover

Expected input

Format:

ACL2s/Lisp file

Internals

Uses ACL2

Comments

ACL2s has been developed because ACL2 had a steep learning curve. The idea being that ACL2s should be easier to use for new users.
Plugin

Links

Project page: http://acl2s.ccs.neu.edu/acl2s/doc/

Last commit date

08 January 2018 (last release date mentioned in release notes)

Related papers

https://doi.org/10.1007/978-3-642-19835-9_27 (TACAS '11)

Last publication date

2011

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.