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

Mathematics Subject Classification ID

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)

Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ Unnamed Item

Uses Software

• Memorax

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