examples of ACL2 scripts
Major Section:  ACL2-TUTORIAL

Beginning users may find these annotated scripts useful. We suggest that you read these in the following order:


The page contains a script that illustrates how it feels to use The Method to prove an unusual list reverse function correct. The screen shots of ACL2's proof output are outdated -- in the version shown, ACL2 does not print Key Checkpoints, but the concept of key checkpoint is clear in the discussion and the behavior of the user.

At is the demo given by Matt Kaufmann at TPHOLs08, including all the scripts. There is a gzipped tar file containing the entire contents of the demos.

At is a collection of scripts illustrating both high-level strategy and lower-level tactics dealing with the functional equivalence of various list sorting algorithms. Start with the README on that directory. There is also a gzipped tar file containing all the scripts.

Some Related Topics