Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses

DOI10.1007/978-3-540-70545-1_13MaRDI QIDQ3512488zbMATH OpenOpenAlexFDO

Authors Ariel Cohen, Amir Pnueli, Lenore D. Zuck

Publication date 15 July 2008

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-70545-1_13

Mathematics Subject Classification ID

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

Recommendations

• Towards formally specifying and verifying transactional memory
• A framework for formally verifying software transactional memory algorithms
• Model checking transactional memories
• Proving opacity of a pessimistic STM
• Verification of STM on relaxed memory models

Cited in

(5)

• Model checking transactional memories
• A framework for formally verifying software transactional memory algorithms
• Completeness and Nondeterminism in Model Checking Transactional Memories
• Verification of STM on relaxed memory models
• Towards formally specifying and verifying transactional memory

Describes a project that uses

Uses Software

• TLPVS

This page was built for publication: Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3512488)