A mechanized refinement proof of the Chase-Lev deque using a proof system

DOI10.1007/s00607-018-0635-4zbMath1458.68276OpenAlexW4242282547WikidataQ129608023 ScholiaQ129608023MaRDI QIDQ2218426

Suha Orhun Mutluergil, Serdar Tasiran

Publication date: 15 January 2021

Published in: Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00607-018-0635-4

zbMATH Keywords

reductionrefinementlinearizabilityabstractionstatic verificationChase-Lev dequeOwicki-Gries method

Mathematics Subject Classification ID

Parallel algorithms in computer science (68W10) Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• An axiomatic proof technique for parallel programs
• A Scalable, Correct Time-Stamped Stack
• Reduction
• A calculus of atomic actions
• Thread scheduling for multiprogrammed multiprocessors

This page was built for publication: A mechanized refinement proof of the Chase-Lev deque using a proof system