ACL2 DEMO GIVEN AT TPHOLs 2008

This is the demo given at TPHOLs in August, 2008. All files discussed below are available in a gzipped tarfile.

You can also find here a plain text file that served as slides for the talk.

The demo consists of the following three parts.

• perm-rev.lisp
  The above file, perm-rev.lisp, contains a demo together with solutions to the various problems encountered when trying to complete the proof. See file perm-rev-exercise.lisp if you want to try working through the demo yourself without the ``answers'', and in the other direction, see file perm-rev-book.lisp for a nice certifiable book based on this demo.

  This demo develops a proof that the reverse of a list is a permutation of the list. It illustrates how to use ACL2 interactively, emphasizing top-down proof development (see :DOC the-method), employing skip-proofs and undoing (see :DOC ubt), and using simplification checkpoints to debug proof failures with gag-mode. This demo also illustrates proof automation using congruence-based conditional rewriting, library development, and local scopes.

• jvm-demo/
  File demo.script in the above directory demonstrates the M5 model of the Java Virtual Machine (JVM). In the process we illustrate several aspects of ACL2. This demo illustrates the use of libraries, packages (see :DOC defpkg) supporting namespaces, efficient evaluation of models, and macros for user-defined syntax (see :DOC defmacro).

• dmr.lisp
  This short demo illustrates management of theories in ACL2 using feedback from the tool, in particular the accumulated-persistence utility and a utility for dynamic monitoring of the rewrite stack.