• Towards automatic proofs of lo...

Treffer: Towards automatic proofs of lock-free algorithms

Title:
Towards automatic proofs of lock-free algorithms
Authors:
Fejoz, Loïc, Merz, Stephan
Contributors:
Proof-oriented development of computer-based systems (MOSEL), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), This work was supported by Microsoft Research through its European PhD Scholarship Programme.
Source:
Exploiting Concurrency Efficiently and Correctly, Jul 2008, Princeton, United States
Publisher Information:
CCSD, 2008.
Publication Year:
2008
Collection:
collection:CNRS
collection:INRIA
collection:INPL
collection:INRIA-LORRAINE
collection:LORIA2
collection:INRIA-NANCY-GRAND-EST
collection:TESTALAIN1
collection:UNIV-LORRAINE
collection:INRIA2
collection:LORIA
collection:INRIA-300009
collection:AM2I-UL
Subject Terms:
lock-free, algorithm, correctness, refinement, ACM: I.: Computing Methodologies, I.6: SIMULATION AND MODELING, I.6.4: Model Validation and Analysis, [INFO.INFO-LO]Computer Science [cs], Logic in Computer Science [cs.LO], [INFO.INFO-DS]Computer Science [cs], Data Structures and Algorithms [cs.DS]
Subject Geographic:
Princeton, United States
Original Identifier:
HAL:
Document Type:
Konferenz conferenceObject<br />Conference papers
Language:
English
Access URL:
https://inria.hal.science/inria-00285752
https://inria.hal.science/inria-00285752v1/document
https://inria.hal.science/inria-00285752v1/file/ec2-08-fejoz-merz.pdf
Rights:
info:eu-repo/semantics/OpenAccess
Accession Number:
edshal.inria.00285752v1
Database:
HAL

Weitere Informationen

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.