Formal Specification and Proofs for Isolated Protocols

This page documents the KIV specifications and the formal proofs that justify the results of Section 3 of the paper Atomic Actions, and their Refinements to Isolated and Not-So-Isolated Protocols by Richard Banach and Gerhard Schellhorn, submitted to FAC (available from the authors). This page should be read in conjunction with Section 10 of the paper, which gives some information on the formal specification.

To get an overview over the structure of the specifications you can have a look at the development graph. This page gives a bottom-up overview over the content of the specifications.

Used basic libraries:

Here you can find all our publications .

Back to the overview of all KIV projects .
For general informations on KIV and a download site for the whole system refer to this page.



[Impressum] [E-Mail]