Model Checking Software

Directed Model Checking.- Large-Scale Directed Model Checking LTL.- Directed Model Checking with Distance-Preserving Abstractions.- Adapting an AI Planning Heuristic for Directed Model Checking.- Larger Automata and Less Work for LTL Model Checking.- Markovian Systems.- Don’t Know in Probabilistic Systems.- Symbolic Model Checking of Stochastic Systems: Theory and Implementation.- Distributed Model Checking.- Parallel and Distributed Model Checking in Eddy.- Distributed On-the-Fly Model Checking and Test Case Generation.- Advanced Handling of Data Aspects.- Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers.- Symbolic Execution with Abstract Subsumption Checking.- Abstract Matching for Software Model Checking.- Applications.- A Parametric State Space for the Analysis of the Infinite Class of Stop-and-Wait Protocols.- Verification of Medical Guidelines by Model Checking – A Case Study.- Assume–Guarantee.- Towards a Compositional SPIN.- Partial Order Reduction.- Exploiting Symmetry and Transactions for Partial Order Reduction of Rule Based Specifications.- Partial-Order Reduction for General State Exploring Algorithms.- Tool Demonstrations.- A Counterexample-Guided Refinement Tool for Open Procedural Programs.- jMosel: A Stand-Alone Tool and jABC Plugin for M2L(Str).- Model Checking Dynamic States in GROOVE.