Summer School Marktoberdorf 2004

Engineering Theories of Software Intensive Systems

Further Reading and Working Material:

• 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

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