Computer-Aided Reasoning for the Masses: The ACL2 Sedan Experience

Abstract

ACL2 is a powerful system for integrated modeling, simulation, and theorem proving. Think of ACL2 as a finely-tuned racecar. In the hands of experts, it has been used to prove some of the most the complex theorems ever proved about commercially designed systems. Novices, however, tend to have a different experience: they crash and burn. Our motivation in developing ACL2s, the ACL2 Sedan, is to bring computer- aided reasoning to the masses. Our goals are to develop a user- friendly system with the power of ACL2, that makes it possible for new users to quickly, easily learn how to develop and reason about programs. 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 all sections of a required freshman course at Northeastern University to teach over 500 undergraduate students how to reason about programs.

Bio: Pete Manolios is an Associate Professor in the College of Computer and Information Science at Northeastern. He has a B.S . and an M.A. in Computer Science from Brooklyn College and a Ph.D. in Computer Sciences from the University of Texas at Austin. Pete's primary research interest is mechanized formal verification and validation of computing systems. What guides his research is the vision that formal methods can be used to revolutionize the design and implementation of highly reliable, robust, and scalable systems in a variety of important application areas, ranging from large component- based software systems to hardware systems to aerospace systems.