src/HOL/HOLCF/IOA/ABP/Read_me
author wenzelm
Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787 64b47495676d
parent 40774 0437dbc127b3
permissions -rw-r--r--
obsolete;

Isabelle Verification of the Alternating Bit Protocol by 
combining IOA with Model Checking

-------------------------------------------------------------

Correctness.ML contains the proof of the abstraction from unbounded
channels to finite ones.

Check.ML contains a simple ModelChecker prototype checking Spec against 
the finite version of the ABP-protocol.