src/HOL/IOA/ABP/Read_me
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1050 0c36c6a52a1d
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     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.