13. SPIN 2006: Vienna, Austria

Directed Model Checking

• Stefan Edelkamp, Shahid Jabbar:
  Large-Scale Directed Model Checking LTL. 1-18
  
• Klaus Dräger, Bernd Finkbeiner, Andreas Podelski:
  Directed Model Checking with Distance-Preserving Abstractions. 19-34
  
• Sebastian Kupferschmid, Jörg Hoffmann, Henning Dierks, Gerd Behrmann:
  Adapting an AI Planning Heuristic for Directed Model Checking. 35-52
  
• Jaco Geldenhuys, Henri Hansen:
  Larger Automata and Less Work for LTL Model Checking. 53-70
  

Markovian Systems

• Harald Fecher, Martin Leucker, Verena Wolf:
  Don't Know in Probabilistic Systems. 71-88
  
• Matthias Kuntz, Markus Siegle:
  Symbolic Model Checking of Stochastic Systems: Theory and Implementation. 89-107
  

Distributed Model Checking

• Igor Melatti, Robert Palmer, Geoffrey Sawaya, Yu Yang, Robert M. Kirby, Ganesh Gopalakrishnan:
  Parallel and Distributed Model Checking in Eddy. 108-125
  
• Christophe Joubert, Radu Mateescu:
  Distributed On-the-Fly Model Checking and Test Case Generation. 126-145
  

Advanced Handling of Data Aspects

• Alessandro Armando, Jacopo Mantovani, Lorenzo Platania:
  Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers. 146-162
  
• Saswat Anand, Corina S. Pasareanu, Willem Visser:
  Symbolic Execution with Abstract Subsumption Checking. 163-181
  
• Pedro de la Cámara, María-del-Mar Gallardo, Pedro Merino:
  Abstract Matching for Software Model Checking. 182-200
  

Applications

• Guy Edward Gallasch, Jonathan Billington:
  A Parametric State Space for the Analysis of the Infinite Class of Stop-and-Wait Protocols. 201-218
  
• Simon Bäumler, Michael Balser, Andriy Dunets, Wolfgang Reif, Jonathan Schmitt:
  Verification of Medical Guidelines by Model Checking - A Case Study. 219-233
  

Assume-Guarantee

• Corina S. Pasareanu, Dimitra Giannakopoulou:
  Towards a Compositional SPIN. 234-251
  

Partial Order Reduction

• Ritwik Bhattacharya, Steven M. German, Ganesh Gopalakrishnan:
  Exploiting Symmetry and Transactions for Partial Order Reduction of Rule Based Specifications. 252-270
  
• Dragan Bosnacki, Stefan Leue, Alberto Lluch-Lafuente:
  Partial-Order Reduction for General State Exploring Algorithms. 271-287
  

Tool Demonstrations

• Aleksandar Dimovski, Dan R. Ghica, Ranko Lazic:
  A Counterexample-Guided Refinement Tool for Open Procedural Programs. 288-292
  
• Christian Topnik, Eva Wilhelm, Tiziana Margaria, Bernhard Steffen:
  jMosel: A Stand-Alone Tool and jABC Plugin for M2L(Str). 293-298
  
• Harmen Kastenberg, Arend Rensink:
  Model Checking Dynamic States in GROOVE. 299-305