UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Modular verification of a non-blocking stack

Parkinson, M; Bornat, R; O'Hearn, P; (2007) Modular verification of a non-blocking stack. In: (pp. pp. 297-302).

Full text not available from this repository.


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. Copyright © 2007 ACM.

Type: Proceedings paper
Title: Modular verification of a non-blocking stack
ISBN: 1595935754
DOI: 10.1145/1190216.1190261
UCL classification: UCL > School of BEAMS
UCL > School of BEAMS > Faculty of Engineering Science
URI: http://discovery.ucl.ac.uk/id/eprint/1342347
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item