COMPILING INSTRUCTIONS:
-----------------------

1.) Install ACL2. The proof has been compiled completely with version 3.6. Installation instructions can be found at http://www.cs.utexas.edu/~moore/acl2/
2.) Set the ACL2_SYSTEM_BOOKS variable:
	export ACL2_SYSTEM_BOOKS="/xx/books"
    where `xx' is replaced with the installation directory of ACL2.
3.) Change the first line in the Makefile to set the books directory.
4.) Type the following from the directory lispfiles/:
	make

All books in all directories will be certified.


CONTENTS:
---------
This directory contains a formal proof of correctness of a deadlock detection algorithm in wormhole networks. Please note that the code is uncleaned and that this is still work in progress. The proofs are correct and complete, but that is it.

The following files are contained:
	algorithm.lisp:
		Contains the algorithm
	correctness.lisp:
		Contains the proof of correctness of the algorithm
	definitions.lisp"
		Contains the definitions and data structures used in the algorithm.
	GeNoC-*.lisp:
		Generic definitions for networks.
	invariants*.lisp:
		Proof that each step op the algorithm preserves each of the invariants.
		

CONTACT:
--------
For any questions, mail f.verbeek@cs.ru.nl.

