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

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Valmari, Antti (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2006.
• Σειρά: Lecture Notes in Computer Science, 3925
• Θέματα: Computer science.; Software engineering.; Programming languages (Electronic computers).; Computer logic.; Computer Science.; Software Engineering/Programming and Operating Systems.; Software Engineering.; Programming Languages, Compilers, Interpreters.; Logics and Meanings of Programs.

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...

Πίνακας περιεχομένων:

• 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.