HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Towards automatic proofs of lock-free algorithms

Loïc Fejoz 1 Stephan Merz 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The verification of lock-free data structures has traditionally been considered as difficult. We propose a formal model for describing such algorithms. The verification conditions generated from this model can often be handled by automatic theorem provers.
Keywords : refinement algorithm correctness lock-free
Document type :
Conference papers
Complete list of metadata

Cited literature [10 references]  Display  Hide  Download
https://hal.inria.fr/inria-00285752
Contributor : Loïc Fejoz Connect in order to contact the contributor
Submitted on : Friday, June 6, 2008 - 11:12:57 AM
Last modification on : Friday, February 4, 2022 - 3:32:22 AM
Long-term archiving on: : Friday, September 28, 2012 - 3:36:11 PM

File

Vignette du document
ec2-08-fejoz-merz.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00285752, version 1

Collections

CNRS | INRIA | LORIA | UNIV-LORRAINE | INRIA2

Citation

Loïc Fejoz, Stephan Merz. Towards automatic proofs of lock-free algorithms. Exploiting Concurrency Efficiently and Correctly, Jul 2008, Princeton, United States. ⟨inria-00285752⟩

Export

BibTeX TEI DC DCterms EndNote Datacite

Share

Metrics

Record views

76

Files downloads

102

 

Contact                    Legal Notice                    Personal Data