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