Stateless model checking for TSO and PSO

DOI10.1007/s00236-016-0275-0zbMath1380.68265OpenAlexW2466104094MaRDI QIDQ1683934

Konstantinos Sagonas, Mohamed Faouzi Atig, Bengt Jonsson, Stavros Aronis, Carl Leonardsson, Parosh Aziz Abdulla

Publication date: 1 December 2017

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00236-016-0275-0

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (10)

Stateless model checking under a reads-value-from equivalence ⋮ Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ Verification of Concurrent Programs on Weak Memory Models ⋮ Stateless model checking for TSO and PSO ⋮ Making Linearizability Compositional for Partially Ordered Executions ⋮ A pragmatic approach to stateful partial order reduction ⋮ Reachability of scope-bounded multistack pushdown systems ⋮ Unnamed Item ⋮ Operational semantics with semicommutations

Uses Software

• veriSoft
• Checkfence

Cites Work

• Unnamed Item
• Analyses and optimizations for shared address space programs.
• Myths about the mutual exclusion problem
• Stateless model checking for TSO and PSO
• State space reduction using partial order techniques
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Counter-Example Guided Fence Insertion under TSO
• Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models
• Effective Program Verification for Relaxed Memory Models
• Dynamic partial-order reduction for model checking software
• Software Verification for Weak Memory via Program Transformation
• Checking and Enforcing Robustness against TSO
• Optimal dynamic partial order reduction

This page was built for publication: Stateless model checking for TSO and PSO