Verification of Opacity of a Transactional Mutex Lock

This page documents the KIV proofs for verifying opacity of a transactional mutex lock. They are based (and assume the reader is familiar with) the explanations given in [FM15]. The overview over the specification structure can be used to browse through specifications, theorems and proofs. Here is a bottom-up explanation.

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.


Bibliography

[FM15] J. Derrick, B. Dongol, G. Schellhorn, O. Travkin, H. Wehrheim.
Verifying Opacity of a Transactional Mutex Lock.
(submitted to FM 2015, draft available from the authors)