The automatic detection of token structures and invariants using SAT checking

DOI10.1007/978-3-662-54580-5_15MaRDI QIDQ3303932zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• scientific article; zbMATH DE number 4053002
• Parametric Deadlock-Freeness Checking Timed Automata
• Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving
• Reachability analysis on distributed executions
• scientific article; zbMATH DE number 910719

Cites work

• scientific article; zbMATH DE number 5139161 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• A Proof System for Communicating Sequential Processes
• Analyzing component-based systems on the basis of architectural constraints
• FDR3 -- a modern refinement checker for CSP
• Lazy reachability analysis in distributed systems
• Proving the Correctness of Multiprocess Programs
• Rigorous development of component-based systems using component metadata and patterns
• Tighter reachability criteria for deadlock-freedom analysis
• Understanding concurrent systems
• Verification, Model Checking, and Abstract Interpretation

Cited in

(3)

• Discovering and correcting a deadlock in a channel implementation
• Mitigating multi-target attacks in hash-based signatures
• Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving

Describes a project that uses

Uses Software

• FDR3

This page was built for publication: The automatic detection of token structures and invariants using SAT checking

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