FDR3 — A Modern Refinement Checker for CSP

DOI10.1007/978-3-642-54862-8_13zbMath1392.68300OpenAlexW1882160752MaRDI QIDQ5498738

A. W. Roscoe, Thomas Gibson-Robinson, Philip Armstrong, Alexandre Boulgakov

Publication date: 10 February 2015

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-54862-8_13

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Sound reasoning in \textit{tock}-CSP ⋮ Testing using CSP Models: Time, Inputs, and Outputs ⋮ Tracking CSP computations ⋮ Process Algebra and Model Checking ⋮ Behavioural Models for FMI Co-simulations ⋮ Rigorous development of component-based systems using component metadata and patterns ⋮ Temporal reasoning through automatic translation of tock-CSP into timed automata ⋮ Refinement-Based Verification of Communicating Unstructured Code ⋮ Unnamed Item ⋮ Translating between models of concurrency ⋮ Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving ⋮ Revisiting sequential composition in process calculi ⋮ Checking opacity and durable opacity with FDR ⋮ Automatic generation of verified concurrent hardware using VHDL ⋮ Simulation relations and applications in formal methods ⋮ Correct and efficient antichain algorithms for refinement checking ⋮ Compositional and local livelock analysis for CSP ⋮ The symbiosis of concurrency and verification: teaching and case studies ⋮ The Automatic Detection of Token Structures and Invariants Using SAT Checking ⋮ Reducing complex CSP models to traces via priority ⋮ Computing maximal weak and other bisimulations ⋮ Ensuring liveness properties of distributed systems: open problems ⋮ View abstraction for systems with component identities ⋮ Mitigating Multi-target Attacks in Hash-Based Signatures ⋮ The expressiveness of CSP with priority ⋮ Discovering and correcting a deadlock in a channel implementation ⋮ Interactive verification of architectural design patterns in FACTum ⋮ Compositional Assume-Guarantee Reasoning of Control Law Diagrams Using UTP ⋮ Compositional verification of asynchronous concurrent systems using CADP

Uses Software

• FDR3