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:
Talk notes:
info-flow-talk.txt
Supporting Lisp file (defines the machine used in the second file, below):
tiny.lisp
Supporting Lisp file:
info-flow-cutpoints-5.lisp