SAT-solving in CSP trace refinement

DOI10.1016/j.scico.2011.07.008zbMath1243.68216OpenAlexW2104703296MaRDI QIDQ436423

A. W. Roscoe, Hristina Palikareva, Joël Ouaknine

Publication date: 20 July 2012

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2011.07.008

zbMATH Keywords

process algebraCSPconcurrencysafety propertiesbounded model checkingFDR\(k\)-inductionSAT-solving

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) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (3)

Tracking CSP computations ⋮ Process Algebra and Model Checking ⋮ Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving

Uses Software

• MiniSat
• NuSMV
• Casper
• PicoSAT
• FDR2
• MAGIC

Cites Work

• An attack on the Needham-Schroeder public-key authentication protocol
• Symbolic model checking: \(10^{20}\) states and beyond
• Understanding concurrent systems
• Concurrent software verification with states, events, and deadlocks
• The expressiveness of CSP with priority
• Unbounded Non-determinism in CSP
• Theory and Applications of Satisfiability Testing
• Communicating Sequential Processes. The First 25 Years
• Theory and Applications of Satisfiability Testing
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: SAT-solving in CSP trace refinement