| author | wenzelm |
| Sat, 14 Oct 2006 23:25:51 +0200 | |
| changeset 21032 | a4b85340d6bd |
| parent 3072 | a31419014be5 |
| 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.