Home
Lectures
Abstracts available
Author Hints
Slides
Picture Book
Application Form
Deadline February 27, 2004
2003
2005
2006
With a click on the button above, your browser will establish a connection to Facebook.
See the Impressum for more information.
|
Further Reading and Working Material:
Little (but Hard) Theorems about Big Systems: Some Case Studies
J Strother Moore
Department of Computer Sciences,
University of Texas at Austin
email: moore@cs.utexas.edu
home page: http://www.cs.utexas.edu/users/moore
- It would be convenient if students would read the following before arriving:
B. Brock and M. Kaufmann and J S. Moore,
Theorems about Commercial Microprocessors,
in "Formal Methods in Computer-Aided Design (FMCAD'96)", M. Srivas and A. Camilleri (eds), LNCS 1166,
Springer Verlag, 1996, pp. 275--293
A version of this available at:
http://www.cs.utexas.edu/users/moore/publications/bkm96.ps.gz
- In addition, it would help to read:
A Gentle Introduction to ACL2 Programming
which is available online at
http://www.cs.utexas.edu/users/moore/publications/gentle-intro-to-acl2-programming.html
- Access to ACL2 during the Summer School will NOT be necessary;
but some students might enjoy experimenting with ACL2 and might want to install it
on a laptop to bring with them.
Also, all students would be helped if they used ACL2 a little, just to understand the setting of the lectures.
- If students have access to a system on which they can install ACL2, they
would be helped if they built ACL2 and experimented with it, following the
directions on the ACL2 home page
http://www.cs.utexas.edu/users/moore/acl2
specifically at the link labeled "Obtaining and Installing Version 2.8".
- After obtaining a runnable version of ACL2, students should do the
programming exercises in
Getting Started with ACL2 Programming
http://www.cs.utexas.edu/users/moore/publications/acl2-programming-exercises1.html
These exercises do NOT teach you how to use the theorem prover, just how to
define functions! But you must understand the language I will use if you are
to understand the theorems I write.
- If you want to learn how to use ACL2 to PROVE theorems instead of just STATE
them, here is a simple example: .
Define the following function for reversing a true-list (a list that "ends in nil''):
(defun rev (x) (if (endp x) nil (append (rev (cdr x)) (list (car x)))))
Then, try to prove
(defthm triple-rev (equal (rev (rev (rev a))) (rev a)))
You might want to refer to the documentation topic called THE-METHOD
in the ACL2 online User's Manual (see the home page).
Hint : It helps to know that when you prove a lemma such as
(defthm associativity-of-foo
(equal (foo (foo a b) c)
(foo a (foo b c))))
ACL2 will henceforth automatically use it as a rewrite rule and will
replace every instance of (foo (foo a b) c) by the corresponding
instance of the (foo a (foo b c)). If the lemma has hypotheses, the
conclusion is used as a rewrite rule whenever the hypotheses can be
REWRITTEN to true. So the lemma
(defthm foo-sometimes-has-an-identity
(implies (true-listp x)
(equal (foo x nil) x)))
will configure the theorem prover so that if it ever encounters an instance
of (foo x nil) it will rewrite it to the corresponding instance of x provided
it can rewrite (true-listp x) to true.
- Now try to prove triple-rev. You'll have to prove some lemmas to make
the theorem prover succeed!
- References : (After some of them URLs are given where
postscript versions of the papers may be found)
M. Kaufmann, P. Manolios, J S. Moore,
Computer-Aided Reasoning: An Approach
Kluwer Academic Press, Boston, MA, 2000
Editors: M. Kaufmann, P. Manolios, J S. Moore,
Computer-Aided Reasoning: ACL2 Case Studies
Kluwer Academic Press, Boston, MA, 2000
B. Brock, J S. Moore,
A Mechanically Checked Proof of a Comparator Sort Algorithm
1999
http://www.cs.utexas.edu/users/moore/publications/csort/main.ps.gz
J S. Moore, T. Lynch, M. Kaufmann,
A Mechanically Checked Proof of the Correctness of the
Kernel of the AMD5K86 Floating Point Division Algorithm
in "IEEE Transactions on Computers", volume 47, number 9, pp. 913-926, 1998
http://www.cs.utexas.edu/users/moore/publications/divide_paper.ps.gz
D. Russinoff,
A Mechanically Checked Proof of IEEE Compliance of a Register-Transfer-Level
Specification of the AMD-K7 Floating-Point Multiplication, Division, and Square
Root Instructions
in "London Mathematical Society Journal of Computation and Mathematics", volume 1, pp. 148-200, 1998
http://www.onr.com/user/russ/david/k7-div-sqrt.html
H. Liu and J S. Moore,
Executable JVM Model for Analytical Reasoning: A Study
in "Workshop on Interpreters, Virtual Machines and Emulators 2003 (IVME '03)", ACM SIGPLAN, San Diego, CA, 2003
http://www.cs.utexas.edu/users/moore/publications/jvm_simulator_in_lisp_0528.ps
|