Proving linearizability with Temporal Logic

S. Bäumler, G. Schellhorn, M. Balser, W. Reif

Proving Linearizability with Temporal Logic

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.

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