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.

    1. 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".


    2. 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.


    3. 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.


    4. 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


Feel free to contact us via e-mail

Phone: (+89) 289 - 17829
Fax: (+89) 289 - 17307

 
Postal address:
Institut für Informatik
Technische Universität München
- Summer School -
Boltzmannstr. 3
85748 Garching (München)

Impressum