The Automatic Detection of Token Structures and Invariants Using SAT Checking

DOI10.1007/978-3-662-54580-5_15zbMath1453.68109OpenAlexW2600980051MaRDI QIDQ3303932

Thomas Gibson-Robinson, A. W. Roscoe, Pedro Antonino

Publication date: 5 August 2020

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

Full work available at URL: https://ora.ox.ac.uk/objects/uuid:3a1db064-937f-40ea-9fb2-749c47bd593f

Mathematics Subject Classification ID

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

Related Items

Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving ⋮ Mitigating Multi-target Attacks in Hash-Based Signatures ⋮ Discovering and correcting a deadlock in a channel implementation

Uses Software

• FDR3

Cites Work

• Unnamed Item
• Unnamed Item
• Rigorous development of component-based systems using component metadata and patterns
• Understanding concurrent systems
• Tighter reachability criteria for deadlock-freedom analysis
• Analyzing Component-Based Systems on the Basis of Architectural Constraints
• A Proof System for Communicating Sequential Processes
• Proving the Correctness of Multiprocess Programs
• Lazy Reachability Analysis in Distributed Systems
• FDR3 — A Modern Refinement Checker for CSP
• Verification, Model Checking, and Abstract Interpretation