Panagiotis (Pete) Manolios
College of Computer and Information Science
Northeastern University

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