Sciweavers

POPL
2007
ACM

Modular verification of a non-blocking stack

14 years 3 months ago
Modular verification of a non-blocking stack
This paper contributes to the development of techniques for the modular proof of programs that include concurrent algorithms. We present a proof of a non-blocking concurrent algorithm, which provides a shared stack. The inter-thread interference, which is essential to the algorithm, is confined in the proof and the specification to the modular operations, which perform push and pop on the stack. This is achieved by the mechanisms of separation logic. The effect is that inter-thread interference does not pollute specification or verification of clients of the stack. Categories and Subject Descriptors D.2.4 [Software Engineering]: Program Verification--correctness proofs, formal methods validation; F.3.1 [Logics and meanings of programs]: Specifying, Verifying and Reasoning about Programs General Terms Languages, Theory, Verification Keywords Separation Logic, Concurrency, Non-blocking
Matthew J. Parkinson, Richard Bornat, Peter W. O'H
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where POPL
Authors Matthew J. Parkinson, Richard Bornat, Peter W. O'Hearn
Comments (0)