The ACL2 Sedan Theorem Proving System
Harsh Raju Chamarthi, Peter Dillinger, Panagiotis Manolios, and Daron Vroon.
TACAS, 2011 © Springer
Abstract
The ACL2 Sedan theorem prover (ACL2s) is an Eclipse plugin that provides a modern integrated development environment, supports
several modes of interaction, provides a powerful termination analysis
engine, and includes fully automatic bug-finding methods based on a
synergistic combination of theorem proving and random testing. ACL2s
is publicly available and open source. It has also been used in several
sections of a required freshman course at Northeastern University to
teach over 200 undergraduate students how to reason about programs.
PDF (87K) © Springer