Parameterized verification under TSO with data types

DOI10.1007/978-3-031-30823-9_30zbMATH Open1543.68186MaRDI QIDQ6535379

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

Publication date: 13 December 2023

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)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Iterated stack automata and complexity classes
• Algorithmic analysis of programs with well quasi-ordered domains.
• Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems
• Parameterized model checking on the TSO weak memory model
• Parameterized compositional model checking
• Taming release-acquire consistency
• Reachability in Higher-Order-Counters
• Parameterised Pushdown Systems with Non-Atomic Writes
• Model-Checking of Ordered Multi-Pushdown Automata
• All for the Price of Few
• Reachability for Dynamic Parametric Processes
• A Perfect Model for Bounded Verification
• Model Checking Procedural Programs
• Model Checking Parameterized Systems
• Parameterized Verification of Asynchronous Shared-Memory Systems
• Emptiness of Multi-pushdown Automata Is 2ETIME-Complete
• Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification
• Parameterized Verification of Ad Hoc Networks
• Reasoning about systems with many processes
• Decidability of Parameterized Verification
• Computer Science Logic
• Checking and Enforcing Robustness against TSO
• Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable
• Correct Hardware Design and Verification Methods
• Computer Aided Verification
• Reachability Analysis of Communicating Pushdown Systems
• Well-structured transition systems everywhere!
• Symbolic model checking with rich assertional languages
• Regular model checking: evolution and perspectives
• Parameterized Verification under Release Acquire is PSPACE-complete

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