Parameterized verification under TSO with data types
From MaRDI portal
Publication:6535379
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
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