Thread-Local, Step-Local Proof Obligations for Refinement of State-Based Concurrent Systems

Gerhard Schellhorn, Stefan Bodenmüller, Wolfgang Reif
Digital Printed Abstract View Cite
Type
Conference paper
Publication
9th International Conference on Rigorous State Based Methods (ABZ'23)

Abstract

This paper presents a proof technique for proving refinements for general state-based models of concurrent systems that reduces proving forward simulations to thread-local, step-local proof obligations. Instances of this proof technique should be applicable to systems specified with ASM rules, B events, or Z operations. To exemplify the proof technique, we demonstrate it with a simple case study that verifies linearizability of a lock-free implementation of concurrent hash sets by showing that it refines an abstract concurrent system with atomic operations. Our theorem prover KIV translates programs to a set of transition rules and generates proof obligations according to the technique.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{SchellhornBR23,
  author       = {Gerhard Schellhorn and
                  Stefan Bodenm{\"{u}}ller and
                  Wolfgang Reif},
  editor       = {Uwe Gl{\"{a}}sser and
                  Jos{\'{e}} Creissac Campos and
                  Dominique M{\'{e}}ry and
                  Philippe A. Palanque},
  title        = {Thread-Local, Step-Local Proof Obligations for Refinement of State-Based
                  Concurrent Systems},
  booktitle    = {Rigorous State-Based Methods - 9th International Conference, {ABZ}
                  2023, Nancy, France, May 30 - June 2, 2023, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14010},
  pages        = {70--87},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-33163-3\_6},
  doi          = {10.1007/978-3-031-33163-3\_6},
  timestamp    = {Mon, 26 Jun 2023 20:49:09 +0200},
  biburl       = {https://dblp.org/rec/conf/zum/SchellhornBR23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'23

Related