Model Checking Software 13th International SPIN Workshop, Vienna, Austria, March 30 - April 1, 2006, Proceedings / edited by Antti Valmari.

The name “SPIN” refers both to a workshopon model checking and to a famous model checking tool. The SPIN workshop is an annual forum for practitioners and researchersinterested in state space-based techniques for the validation and analysis of software and hardware systems, including communication p...

Full description

Saved in:
Bibliographic Details
Corporate Author: SpringerLink (Online service)
Other Authors: Valmari, Antti (Editor)
Format: eBook
Language:English
Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2006.
Edition:1st ed. 2006.
Series:Theoretical Computer Science and General Issues ; 3925
Springer eBook Collection.
Subjects:
Online Access:Click to view e-book
Holy Cross Note:Loaded electronically.
Electronic access restricted to members of the Holy Cross Community.
Table of Contents:
  • 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.