src/HOL/HOLCF/IOA/ABP/Read_me
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 3072 src/HOLCF/IOA/ABP/Read_me@a31419014be5
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
     1 Isabelle Verification of the Alternating Bit Protocol by 
     2 combining IOA with Model Checking
     3 
     4 -------------------------------------------------------------
     5 
     6 Correctness.ML contains the proof of the abstraction from unbounded
     7 channels to finite ones.
     8 
     9 Check.ML contains a simple ModelChecker prototype checking Spec against 
    10 the finite version of the ABP-protocol.