| author | wenzelm |
| Mon, 27 Jan 1997 09:08:54 +0100 | |
| changeset 2556 | bef8e1315cbc |
| parent 1050 | 0c36c6a52a1d |
| 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.