 |
Description
``ACL2'' stands for ``A Computational Logic for Applicative Common Lisp.''
It is a functional programming language, a mathematical logic and a mechanical
theorem prover for that logic. ACL2 is used to model computing systems
-- both hardware and software -- and to prove properties of those models.
The ACL2 home page is http://www.cs.utexas.edu/users/moore/acl2.
ACL2 is used primarily in industry to prove properties of microprocessors.
For example, the IEEE compliance of the RTL implementing the elementary
floating-point operations on the AMD Athlon (TM) microprocessor was proved
by David Russinoff using ACL2, and ACL2 was used at Rockwell-Collins to
model the JEM1 microprocessor, the world's first silicon Java Virtual
Machine. These and many other applications are described in http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html.
In this class you will learn how to use ACL2. The class will start with
an introduction to Lisp and to ACL2. You will then be given elementary
exercises to do with ACL2 and we will gradually build up to more elaborate
examples such as the modelling of simple programming languages, compilers,
and architectures.
|
|
