The ACL2 Sedan theorem prover (ACL2s) is an Eclipse plug-in 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. © 2011 Springer-Verlag.
CITATION STYLE
Chamarthi, H. R., Dillinger, P., Manolios, P., & Vroon, D. (2011). The ACL2 Sedan theorem proving system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6605 LNCS, pp. 291–295). https://doi.org/10.1007/978-3-642-19835-9_27
Mendeley helps you to discover research relevant for your work.