Survey on Directed Model Checking

DOI10.1007/978-3-642-00431-5_5MaRDI QIDQ3614878zbMATH OpenOpenAlexFDO

Authors Stefan Edelkamp, Viktor Schuppan, Dragan Bošnački, Anton Wijs, Ansgar Fehnker, Husain Aljazzar

Publication date 17 March 2009

Published in Model Checking and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-00431-5_5

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Transition-Based Directed Model Checking
• The Causal Graph Revisited for Directed Model Checking
• scientific article; zbMATH DE number 2087625
• Directed Model Checking for B: An Evaluation and New Techniques
• Model Checking Software

Cites work

• 25 years of model checking. History, achievements, perspectives
• A logic for reasoning about time and reliability
• A note on two problems in connexion with graphs
• A Recovering Beam Search algorithm for the one-machine dynamic total completion time scheduling problem
• A result on the computational complexity of heuristic estimates for the A^* algorithm
• A theory of timed automata
• AI 2003: Advances in Artificial Intelligence
• Algorithms for memory hierarchies. Advanced lectures
• Automata-theoretic techniques for modal logics of programs
• Breadth-first heuristic search
• Combining partial-order reductions with on-the-fly model-checking.
• Compositional SCC analysis for language emptiness
• Computer Aided Verification
• Counterexamples in Probabilistic Model Checking
• Depth-first iterative-deepening: An optimal admissible tree search
• Distributed Extended Beam Search for Quantitative Model Checking
• Extended Directed Search for Probabilistic Timed Reachability
• Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words
• Formal Modeling and Analysis of Timed Systems
• Frontier search
• Generalized best-first search strategies and the optimality of A*
• Grammar Analysis and Parsing by Abstract Interpretation
• Heuristic Search for the Analysis of Graph Transition Systems
• scientific article; zbMATH DE number 1670553 (Why is no real title available?)
• scientific article; zbMATH DE number 1670790 (Why is no real title available?)
• scientific article; zbMATH DE number 1701758 (Why is no real title available?)
• scientific article; zbMATH DE number 177248 (Why is no real title available?)
• scientific article; zbMATH DE number 729460 (Why is no real title available?)
• scientific article; zbMATH DE number 734956 (Why is no real title available?)
• scientific article; zbMATH DE number 1069483 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 1982194 (Why is no real title available?)
• scientific article; zbMATH DE number 1487475 (Why is no real title available?)
• scientific article; zbMATH DE number 2086969 (Why is no real title available?)
• scientific article; zbMATH DE number 2087625 (Why is no real title available?)
• scientific article; zbMATH DE number 2102708 (Why is no real title available?)
• Interpolation and SAT-based model checking.
• Job shop scheduling with beam search
• Lectures on Concurrency and Petri Nets
• Liveness checking as safety checking for infinite state spaces
• Model Checking Software
• Model Checking Software
• Model-checking continuous-time Markov chains
• On a routing problem
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Partial-order reduction in symbolic state-space exploration
• Providing Evidence of Likely Being on Time: Counterexample Generation for CTMC Model Checking
• Pruning State Spaces with Extended Beam Search
• Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking
• Scheduling with timed automata
• Semi-external LTL Model Checking
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(17)

• Wireless protocol validation under uncertainty
• Automata-driven partial order reduction and guided search for LTL model checking
• Directed reachability for infinite-state systems
• Directed Model Checking for B: An Evaluation and New Techniques
• Abstractions and pattern databases: the quest for succinctness and accuracy
• The Causal Graph Revisited for Directed Model Checking
• Transition-Based Directed Model Checking
• Hierarchical Adaptive State Space Caching Based on Level Sampling
• scientific article; zbMATH DE number 1746648 (Why is no real title available?)
• Formal verification of concurrent systems via directed model checking
• Fast Directed Model Checking Via Russian Doll Abstraction
• Verification, Model Checking, and Abstract Interpretation
• Model Checking Software
• Model Checking Software
• Flash memory efficient LTL model checking
• Extended beam search for non-exhaustive state space analysis
• A local search approach to protocol verification

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: Survey on Directed Model Checking

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