Context-Bounded Analysis of TSO Systems
DOI10.1007/978-3-642-54848-2_2zbMath1416.68050OpenAlexW93329440MaRDI QIDQ5170741
Mohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato
Publication date: 24 July 2014
Published in: From Programs to Systems. The Systems perspective in Computing (Search for Journal in Brave)
Full work available at URL: https://eprints.soton.ac.uk/365362/1/WMM.pdf
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (2)
Uses Software
Cites Work
- Unnamed Item
- What’s Decidable about Weak Memory Models?
- Counter-Example Guided Fence Insertion under TSO
- Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models
- Deciding Robustness against Total Store Ordering
- Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
- Effective Program Verification for Relaxed Memory Models
- Formalising Java’s Data Race Free Guarantee
- Emptiness of Multi-pushdown Automata Is 2ETIME-Complete
- Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads
- Reducing Context-Bounded Concurrent Reachability to Sequential Reachability
- On the verification problem for weak memory models
- Relaxed memory models
- Software Verification for Weak Memory via Program Transformation
- Checking and Enforcing Robustness against TSO
- The tree width of auxiliary storage
- Interprocedural Analysis of Concurrent Programs Under a Context Bound
- Tools and Algorithms for the Construction and Analysis of Systems
- Scope-Bounded Pushdown Languages
This page was built for publication: Context-Bounded Analysis of TSO Systems