SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR

DOI10.1007/978-3-540-69850-0_13zbMath1142.68440OpenAlexW1603832849MaRDI QIDQ3512442

Joseph Sifakis, J. P. Queille

Publication date: 15 July 2008

Published in: 25 Years of Model Checking (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-69850-0_13

zbMATH Keywords

CSPvalidationcommunicating sequential processesalgorithmic descriptionfixed points of monotonic predicate transformersinterpreted Petri net

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Checking interval properties of computations ⋮ Model checking of pushdown systems for projection temporal logic ⋮ Unnamed Item ⋮ Generating counterexamples for quantitative safety specifications in probabilistic B ⋮ Linear temporal logic symbolic model checking ⋮ Verifying a Network Invariant for All Configurations of the Futurebus+ Cache Coherence Protocol ⋮ Verifying untimed and timed aspects of the experimental batch plant ⋮ More Precise Partition Abstractions ⋮ Mechanical Software Verification ⋮ Is your model checker on time? On the complexity of model checking for timed modal logics

Uses Software

• CESAR

Cites Work

• The temporal logic of branching time
• A unified approach for studying the properties of transition systems
• Formal semantics of a class of high-level primitives of coordinating concurrent processes
• Synthesis of Resource Invariants for Concurrent Programs
• Formal verification of parallel programs
• Communicating sequential processes
• Distributed processes
• Unnamed Item
• Unnamed Item
• Unnamed Item