Formal verification of concurrent systems via directed model checking

DOI10.1016/J.ENTCS.2007.05.031MaRDI QIDQ5178996zbMATH OpenOpenAlexFDO

Authors Sara Gradara, Antonella Santone, Maria Luisa Villani

Publication date 18 March 2015

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2007.05.031

zbMATH Keywords

CCSheuristic searchmodel checking

Mathematics Subject Classification ID

Temporal logic (03B44) 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)

Recommendations

• Abstract reduction in directed model checking CCS processes
• Transition-Based Directed Model Checking
• Using heuristic search for finding deadlocks in concurrent systems
• Survey on Directed Model Checking
• scientific article; zbMATH DE number 2087625

Cites work

• \(\text{DELFIN}^+\): an efficient deadlock detection tool for CCS processes
• Automatic verification of concurrent systems using a formula-based compositional approach
• Construction and Analysis of Transition Systems with MEC
• Efficient verification of a multicast protocol for mobile computing
• Guided model checking with a Bayesian meta-heuristic
• scientific article; zbMATH DE number 4180789 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 2080054 (Why is no real title available?)
• scientific article; zbMATH DE number 1746648 (Why is no real title available?)
• scientific article; zbMATH DE number 4119603 (Why is no real title available?)
• Interpolants and Symbolic Model Checking
• Local model checking in the modal mu-calculus
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Selective mu-calculus and formula-based equivalence of transition systems
• Using heuristic search for finding deadlocks in concurrent systems

Cited in

(8)

• Compact and efficiently verifiable models for concurrent systems
• A formal model of concurrent systems based on bipartite directed acyclic graph
• Using heuristic search for finding deadlocks in concurrent systems
• Property Directed Reachability for Proving Absence of Concurrent Modification Errors
• scientific article; zbMATH DE number 967185 (Why is no real title available?)
• Verification, Model Checking, and Abstract Interpretation
• Abstract reduction in directed model checking CCS processes
• \(\text{DELFIN}^+\): an efficient deadlock detection tool for CCS processes

This page was built for publication: Formal verification of concurrent systems via directed model checking

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