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
nipkow@1050
     1
Isabelle Verification of the Alternating Bit Protocol by 
nipkow@1050
     2
combining IOA with Model Checking
nipkow@1050
     3
nipkow@1050
     4
-------------------------------------------------------------
nipkow@1050
     5
nipkow@1050
     6
Correctness.ML contains the proof of the abstraction from unbounded
nipkow@1050
     7
channels to finite ones.
nipkow@1050
     8
nipkow@1050
     9
Check.ML contains a simple ModelChecker prototype checking Spec against 
nipkow@1050
    10
the finite version of the ABP-protocol.