Proving linearizability with Temporal Logic

Proving Linearizability with Temporal Logic

erschienen 17.12.2008 in: Universität Augsburg, Technical Report 2008-19 Technical Report, Institute of Computer Science, University of Augsburg, December 2008

Linearizability is a correctness criterion for concurrent systems. In this report, we describe how temporal logic can be used to prove linearizability of a concurrent lock-free stack implementation. The logic used is an extended variant of Interval Temporal Logic, which is integrated in the KIV interactive theorem prover. To reduce the proof to single components only a compositional reasoning technique is used.

Downloads:

• techreport  -  (2008-lockfree.pdf, 0 KB)