Mechanized proofs of opacity: a comparison of two techniques

DOI10.1007/S00165-017-0433-3zbMath1395.68186OpenAlexW2746481414WikidataQ59528325 ScholiaQ59528325MaRDI QIDQ1673658

Gerhard Schellhorn, Oleg Travkin, John Derrick, Heike Wehrheim, Simon Doherty, Brijesh Dongol

Publication date: 12 September 2018

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-017-0433-3

zbMATH Keywords

verificationrefinementopacityIsabellesoftware transactional memoryKIV

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (2)

Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory ⋮ Checking opacity and durable opacity with FDR

Uses Software

• Isabelle
• Isabelle/HOL
• PVS
• KIV
• NOrec
• RingSTM

Cites Work

• Unnamed Item
• Virtual world consistency: a condition for STM systems (with a versatile protocol with invisible read operations)
• Towards formally specifying and verifying transactional memory
• Isabelle/HOL. A proof assistant for higher-order logic
• Forward and backward simulations. I. Untimed Systems
• Model checking transactional memories
• A Framework for Formally Verifying Software Transactional Memory Algorithms
• A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
• Completeness and Nondeterminism in Model Checking Transactional Memories
• Modular Safety Checking for Fine-Grained Concurrency
• Transactional Memory: Glimmer of a Theory
• The serializability of concurrent database updates
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• A programming language perspective on transactional memory consistency
• Verifying Opacity of a Transactional Mutex Lock
• Formal Techniques for Networked and Distributed Systems – FORTE 2004

This page was built for publication: Mechanized proofs of opacity: a comparison of two techniques