Model-checking of correctness conditions for concurrent objects

DOI10.1006/inco.1999.2847zbMath1003.68067OpenAlexW2672830324MaRDI QIDQ1854357

Rajeev Alur, Doron A. Peled, K. L. McMillan

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/80e1df595a00f2087bc50366b67bfc2554e955e8

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items (16)

On the correctness problem for serializability ⋮ TSO-to-TSO linearizability is undecidable ⋮ Automated Synthesis of Distributed Controllers ⋮ Model checking transactional memories ⋮ On reducing linearizability to state reachability ⋮ Static analysis for detecting high-level races in RTOS kernels ⋮ On Distributed Monitoring and Synthesis ⋮ Decidability and complexity for quiescent consistency and its variations ⋮ On the complexity of linearizability ⋮ Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency ⋮ Concurrent correctness in vector space ⋮ Spiking neural P systems: matrix representation and formal verification ⋮ Deciding Robustness against Total Store Ordering ⋮ Conversation protocols: a formalism for specification and verification of reactive electronic services ⋮ Unnamed Item ⋮ The F-Snapshot Problem

Cites Work

• Unnamed Item
• Unnamed Item
• Maximal serializability of iterated transactions
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• The notions of consistency and predicate locks in a database system
• Characterizations of the decidability of some problems for regular trace languages

This page was built for publication: Model-checking of correctness conditions for concurrent objects