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 <>
Submitted on : Friday, June 6, 2008 - 11:12:57 AM
Last modification on : Friday, February 26, 2021 - 3:28:05 PM
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

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

Share

Metrics

Record views

251

Files downloads

177

 

Contact                    Legal Notice                    Personal Data