SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR

DOI10.1007/978-3-540-69850-0_13MaRDI QIDQ3512442zbMATH OpenOpenAlexFDO

Authors J. P. Queille, Joseph Sifakis

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

algorithmic descriptioncommunicating sequential processesCSPfixed points of monotonic predicate transformersinterpreted Petri netvalidation

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)

Recommendations

• scientific article; zbMATH DE number 47176
• The analysis of concurrent systems. Cambridge, September 12-16, 1983. Proceedings
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• scientific article; zbMATH DE number 3997155
• A functional programming approach to the specification and verification of concurrent systems

Cites work

• A unified approach for studying the properties of transition systems
• Communicating sequential processes
• Distributed processes
• Formal semantics of a class of high-level primitives of coordinating concurrent processes
• Formal verification of parallel programs
• scientific article; zbMATH DE number 3755842 (Why is no real title available?)
• scientific article; zbMATH DE number 3621123 (Why is no real title available?)
• scientific article; zbMATH DE number 3363520 (Why is no real title available?)
• Synthesis of Resource Invariants for Concurrent Programs
• The temporal logic of branching time

Cited in

(15)

• Is your model checker on time? On the complexity of model checking for timed modal logics
• Model checking of pushdown systems for projection temporal logic
• Verifying untimed and timed aspects of the experimental batch plant
• Mechanical software verification: high level control aspects from a user's perspective
• Checking interval properties of computations
• Specifying and Analysing SOC Applications with COWS
• Twenty Years on: Reflections on the CEDISYS Project. Combining True Concurrency with Process Algebra
• Implementations of the CSP Notation for Concurrent Systems
• scientific article; zbMATH DE number 47176 (Why is no real title available?)
• Linear temporal logic symbolic model checking
• Verifying a network invariant for all configurations of the Futurebus+ cache coherence protocol
• scientific article; zbMATH DE number 7438567 (Why is no real title available?)
• More Precise Partition Abstractions
• Generating counterexamples for quantitative safety specifications in probabilistic B
• A functional programming approach to the specification and verification of concurrent systems

Describes a project that uses

Uses Software

• CESAR

This page was built for publication: SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR

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