Index of /users/moore/acl2/books/books/defexec/find-path

 Name                    Last modified      Size  Description
 Parent Directory                             -   
 graph/                  30-Jan-2006 22:00    -   
 Makefile                15-Dec-2005 08:46  279   
 fpst.lisp               14-Dec-2005 22:30   27K  
 run-fpst.lisp           14-Dec-2005 22:30   10K  

These files contain an optimized version of a program that searches
for a path in a graph.  It is the subject of 2 ACL2 workshop papers,
one in 2000 by Matt Wilding and one in 2003 by David Greve and Matt
Wilding, that describe using ACL2 features to build fast and
verifiable software.

A makefile creates books from two files

  fpst.lisp - definition of the optimized pathfinder and proof that 
  it is equivalent to previously distributed version

  run-fpst.lisp - definitions that provide for benchmarking the
  pathfinder

This proof relies upon books developed by J Moore that are freely
available and documented in the chapter "An Exercise in Graph Theory"
in the book "Computer-Aided Reasoning: ACL2 Case Studies".

David Greve
Matt Wilding
June 2003