Parameterized verification under TSO with data types

DOI10.1007/978-3-031-30823-9_30MaRDI QIDQ6535379zbMATH OpenFDO

Authors Parosh A. Abdulla, Mohamad Faouzi Atig, Florian Furbach, Adwait Godbole, Yacoub G. Hendi, Shankara Narayanan Krishna, Stephan Spengler

Publication date 13 December 2023

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-30823-9_30

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Parameterized model checking on the TSO weak memory model
• A load-buffer semantics for total store ordering
• The benefits of duality in verifying concurrent programs under TSO
• scientific article; zbMATH DE number 2080051
• Networks of processes with parameterized state space

Cites work

• A load-buffer semantics for total store ordering
• A perfect model for bounded verification
• Abstract regular tree model checking
• Algorithmic analysis of programs with well quasi-ordered domains.
• All for the price of few (parameterized verification through view abstraction)
• Checking and enforcing robustness against TSO
• Computer Science Logic
• Constrained monotonic abstraction: a CEGAR for parameterized verification
• Decidability of parameterized verification
• Emptiness of Multi-pushdown Automata Is 2ETIME-Complete
• Exact and efficient verification of parameterized cache coherence protocols
• scientific article; zbMATH DE number 3722109 (Why is no real title available?)
• scientific article; zbMATH DE number 1302047 (Why is no real title available?)
• Iterated stack automata and complexity classes
• Iterating transducers in the large (extended abstract)
• Model checking parameterized systems
• Model checking procedural programs
• Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems
• Model-checking of ordered multi-pushdown automata
• Parameterised pushdown systems with non-atomic writes
• Parameterized compositional model checking
• Parameterized model checking on the TSO weak memory model
• Parameterized verification of ad hoc networks
• Parameterized Verification of Asynchronous Shared-Memory Systems
• Parameterized Verification under Release Acquire is PSPACE-complete
• Reachability analysis of communicating pushdown systems
• Reachability for dynamic parametric processes
• Reachability in higher-order-counters
• Reasoning about systems with many processes
• Regular model checking: evolution and perspectives
• Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable
• Symbolic model checking with rich assertional languages
• Taming release-acquire consistency
• Well-structured transition systems everywhere!

Cited in

(3)

• scientific article; zbMATH DE number 7365811 (Why is no real title available?)
• TSO games -- on the decidability of safety games under the total store order semantics
• TSO games -- on the decidability of safety games under the total store order semantics

This page was built for publication: Parameterized verification under TSO with data types

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