summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/IOA/ABP/Read_me

author | nipkow |

Tue Apr 08 10:48:42 1997 +0200 (1997-04-08) | |

changeset 2919 | 953a47dc0519 |

parent 1050 | 0c36c6a52a1d |

permissions | -rw-r--r-- |

Dep. on Provers/nat_transitive

1 Isabelle Verification of the Alternating Bit Protocol by

2 combining IOA with Model Checking

4 -------------------------------------------------------------

6 Correctness.ML contains the proof of the abstraction from unbounded

7 channels to finite ones.

9 Check.ML contains a simple ModelChecker prototype checking Spec against

10 the finite version of the ABP-protocol.