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