A framework for formally verifying software transactional memory algorithms
DOI10.1007/978-3-642-32940-1_36zbMATH Open1365.68163OpenAlexW3741743MaRDI QIDQ2912700FDOQ2912700
Authors: Mohsen Lesani, Victor Luchangco, Mark Moir 
Publication date: 25 September 2012
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-32940-1_36
Recommendations
Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cited In (10)
- Towards formally specifying and verifying transactional memory
- Formalization and correctness of a concurrent linear hash structure algorithm using nested transactions and I/O automata
- Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses
- Proving Isolation Properties for Software Transactional Memory
- Title not available (Why is that?)
- Formal verification of a C-like memory model and its uses for verifying program transformations
- Checking opacity and durable opacity with FDR
- An analytic framework for performance modeling of software transactional memory
- Mechanized proofs of opacity: a comparison of two techniques
- Model checking transactional memories
Uses Software
This page was built for publication: A framework for formally verifying software transactional memory algorithms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2912700)
