| changeset 3072 | a31419014be5 |
| 3071:981258186b71 | 3072:a31419014be5 |
|---|---|
1 Isabelle Verification of the Alternating Bit Protocol by |
|
2 combining IOA with Model Checking |
|
3 |
|
4 ------------------------------------------------------------- |
|
5 |
|
6 Correctness.ML contains the proof of the abstraction from unbounded |
|
7 channels to finite ones. |
|
8 |
|
9 Check.ML contains a simple ModelChecker prototype checking Spec against |
|
10 the finite version of the ABP-protocol. |