`Proceedings of the 13th SPIN Workshop on Model Checking Software Vienna, Austria Co-located with ETAPS 2006 March 30 - April 1, 2006`

Published in:
	Lecture Notes in Computer Science,
	Volume LNCS 3925, Springer Verlag, March 2006

`Invited Presentation:`

Roope Kaivola (Intel), Formal Verification of Industrial Microprocessor Designs

A Counterexample-Guided Refinement Tool for Open Procedural Programs, (PDF)
A. Dimovski (Univ. of Warwick, UK), D.R. Ghica (Univ. of Birmingham, UK), R. Lazic (Univ. of Warwick, UK)
jMosel: A Stand-Alone Tool and jABC Plugin for M2L(Str), (PDF)
C. Topnik (Univ. of Dortmund), E. Wilhelm (Univ. of Dortmund), T. Margaria (Univ. of Göttingen), B. Steffen (Univ. of Dortmund)
CTL Model Checking in GROOVE, (PDF)
H. Kastenberg, A. Rensink (Univ. of Twente, NL)
Directed Model Checking S. Edelkamp (Univ. of Dortmund)

Large-Scale Directed Model Checking LTL, (PDF)
S. Edelkamp, S. Jabbar (Univ. of Dortmund)
Directed Model Checking with Distance-Preserving Abstractions, (PDF)
K. Dräger (Univ. des Saarlandes), B. Finkbeiner (Univ. des Saarlandes), A. Podelski (Max-Planck-Inst.)
Adapting an AI Planning Heuristic for Directed Model Checking, (PDF)
S. Kupferschmid (Univ. of Freiburg), J. Hoffmann (Max-Planck-Inst.), H. Dierks (OFFIS), G. Behrmann (Aalborg Univ., DK)
Larger Automata and Less Work for LTL Model Checking, (PDF)
J. Geldenhuys (Stellenbosch Univ., RSA), H. Hansen (Tampere Univ., Fi)

Don't know in Probabilistic Systems, (PDF)
H. Fecher (Univ. of Kiel), M. Leucker (TU Munich), V. Wolf (Univ. of Mannheim)
Symbolic Model Checking of Stochastic Systems: Theory and Implementation, (PDF)
M. Kuntz, M. Siegle (Univ. of Federal Armed Forces, Munich)

Parallel and Distributed Model Checking in Eddy, (PDF)
I. Melatti, R. Palmer, G. Sawaya, Y. Yang, R.M. Kirby, G. Gopalakrishnan (Univ. of Utah, USA)
Distributed On-the-Fly Model Checking and Test Case Generation, (PDF)
C. Joubert (INRIA Rhone-Alpes/VASY), R. Mateescu (ENS LYON)

Bounded Model Checking of Software using SMT Solvers instead of SAT Solvers, (PDF)
A. Armando, J. Mantovani, L. Platania (Univ. degli Studi di Genova)
Symbolic Execution with Abstract Subsumption Checking, (PDF)
S. Anand (Georgia Inst. Tech.), C.S. Pasareanu (NASA Ames), W. Visser (NASA Ames)
Abstract Matching for Software Model Checking, (PDF)
P. de la Camara, M. del Mar Gallardo, P. Merino (Univ. of Malaga)

A Parametric State Space for the Analysis of the Infinite Class of Stop-and-Wait Protocols, (PDF)
G.E. Gallasch, J. Billington (Univ. of South Australia)
Verification of Medical Guidelines by Model Checking -- A Case Study, (PDF)
S. Bäumler, M. Balser, A. Dunets, W. Reif, J. Schmitt (Univ. of Augsburg)

Towards a Compositional SPIN, (PDF)
C.S. Pasareanu, D. Giannakopoulou (NASA Ames)

Exploiting Symmetry and Transactions for Partial Order Reduction of Rule Based Specifications, (PDF)
R. Bhattacharya (Univ. of Utah, USA), S.M. German (IBM Watson Research Center), G. Gopalakrishnan (Univ. of Utah, USA)
Partial-Order Reduction for General State Exploring Algorithms, (PDF)
D. Bosnacki (Eindhoven Univ.), S. Leue (Univ. of Konstanz), A.L. Lafuente (Empoli, Italy)

Return to Spin Homepage
(Page updated: 14 April 2006)