src/HOL/IOA/ABP/Read_me
author paulson
Mon Oct 07 10:28:44 1996 +0200 (1996-10-07)
changeset 2056 93c093620c28
parent 1050 0c36c6a52a1d
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
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.