ACL2 Theorem Proving Seminar at UT: Information Flow (Jan. 2008)
ACL2 Seminar talks by Robert Krug on 1/23/08 and 1/30/08 are on the topic of information flow and using ACL2 to prove properties about information flow.
Contents of this directory:
Supporting Lisp file (defines the machine used in the second file, below):
Supporting Lisp file: