Efficient Execution in an Automated Reasoning Environment
D. A. Greve, M. Kaufmann, P. Manolios, J S. Moore, S. Ray, J. L. Ruiz-Reina, R. Sumners,
D. Vroon, and M. Wilding
Technical Report TR-06-59, Department of Computer Sciences, University
of Texas at Austin, November 2006.
We describe a method to permit the user of a mathematical logic to write
elegant logical definitions while allowing sound and efficient execution. We
focus on the ACL2 logic and automated reasoning environment. ACL2 is used by
industrial researchers to describe microprocessor designs and other complicated
digital systems. Properties of the designs can be formally established with
the theorem prover. But because ACL2 is also a functional programming
language, the formal models can be executed as simulation engines. We implement
features that afford these dual applications, namely formal proof and execution
on industrial test suites. In particular, the features allow the user to
install, in a logically sound way, alternative executable counterparts for
logically-defined functions. These alternatives are often much more efficient
than the logically equivalent terms they replace. We discuss several
applications of these features.
- Paper (ps, pdf)
- Supporting materials: See the directory
books/defexec/ in the current ACL2 distribution.