author | wenzelm |
Sat, 07 Apr 2012 16:41:59 +0200 | |
changeset 47389 | e8552cba702d |
parent 40774 | 0437dbc127b3 |
permissions | -rw-r--r-- |
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.