SPIN logo

SPIN 2006

13th International SPIN Workshop on Model Checking of Software

March 30 -- April 1, 2006, Vienna, Austria

A satellite workshop of ETAPS 2006

ETAPS 2006 logo

LNCS logo

LNCS 3925 (proceedings) online:
general   the volume

Programme


[What is SPIN] [Registration to the Workshop] [Programme Committee] [Advisory and Steering Committees] [Inquiries] [Call for Papers] [The SPIN Tool Webpage] [LNCS Webpage]

Thursday March 30

10:00 -- 12:00 Joint TACAS/SPIN Tool Session, contains
11:30 -- 12:00
 
A Counterexample-Guided Refinement Tool for Open Procedural Programs
Aleksandar Dimovski (Univ. of Warwick, Coventry, UK), Dan R. Ghica (Univ. of Birmingham, UK), Ranko Lazic (Univ. of Warwick, Coventry, UK)

12:00 -- 14:00

Lunch

14:00 -- 15:00

ETAPS Invited Presentation

15:00 -- 15:15

Break

15:15 -- 16:15

Joint SPIN/TACAS Tool Session (Chair: Susanne Graf), contains
15:15 -- 15:45
 
jMosel: A Stand-Alone Tool and jABC Plugin for M2L(Str)
Christian Topnik (Univ. of Dortmund, D), Eva Wilhelm (Univ. of Dortmund, D), Tiziana Margaria (Univ. of Göttingen, D), Bernhard Steffen (Univ. of Dortmund, D)

16:15 -- 16:45

Break

Tool and Tutorial (Chair: Dragan Bosnacki)
16:45 -- 17:15 
 
Model Checking Dynamic States in GROOVE
Harmen Kastenberg, Arend Rensink (Univ. of Twente, Enschede, NL)
17:15 -- 18:30
 
Tutorial: Directed Model Checking
Stefan Edelkamp (Univ. of Dortmund, D)

Friday March 31

  8:30 --   9:30 ETAPS Invited Presentation

  9:30 -- 10:00

Break

Directed Model Checking (Chair: Stefan Leue)
10:00 -- 10:30 
 
Large-Scale Directed Model Checking LTL
Stefan Edelkamp, Shahid Jabbar (Univ. of Dortmund, D)
10:30 -- 11:00
 
Directed Model Checking with Distance-Preserving Abstractions
Klaus Dräger (Univ. des Saarlandes, Saarbrücken, D), Bernd Finkbeiner (Univ. des Saarlandes, Saarbrücken, D), Andreas Podelski (Max-Planck-Inst. for CS, Saarbrücken, D)
11:00 -- 11:30
 
Adapting an AI Planning Heuristic for Directed Model Checking
Sebastian Kupferschmid (Univ. of Freiburg, D), Jörg Hoffmann (Max-Planck-Inst. for CS, Saarbrücken, D), Henning Dierks (OFFIS, D), Gerd Behrmann (Aalborg Univ., DK)
11:30 -- 12:00
 
Larger Automata and Less Work for LTL Model Checking
Jaco Geldenhuys (Stellenbosch Univ., Matieland, RSA), Henri Hansen (Tampere Univ. of Tech., FI)

12:00 -- 14:00

Lunch

Markovian Systems (Chair: Gianfranco Ciardo)
14:00 -- 14:30
 
Don't know in Probabilistic Systems
Harald Fecher (Univ. of Kiel, D), Martin Leucker (TU Munich, D), Verena Wolf (Univ. of Mannheim, D)
14:30 -- 15:00
 
Symbolic Model Checking of Stochastic Systems: Theory and Implementation
Matthias Kuntz, Markus Siegle (Univ. of Federal Armed Forces, Munich, D)

Distributed Model Checking (Chair: Gianfranco Ciardo)
15:00 -- 15:30
 
Parallel and Distributed Model Checking in Eddy
Igor Melatti, Robert Palmer, Geoffrey Sawaya, Yu Yang, Robert Mike Kirby, Ganesh Gopalakrishnan (Univ. of Utah, USA)
15:30 -- 16:00
 
Distributed On-the-Fly Model Checking and Test Case Generation
Christophe Joubert (INRIA Rhone-Alpes / VASY, F), Radu Mateescu (ENS LYON / LIP / PLUME, F)

16:00 -- 16:30

Break

Advanced Handling of Data Aspects (Chair: Ganesh Gopalakrishnan)
16:30 -- 17:00
 
Bounded Model Checking of Software using SMT Solvers instead of SAT Solvers
Alessandro Armando, Jacopo Mantovani, Lorenzo Platania (Univ. degli Studi di Genova, IT)
17:00 -- 17:30
 
Symbolic Execution with Abstract Subsumption Checking
Saswat Anand (Georgia Inst. Tech., USA), Corina S. Pasareanu (NASA Ames Res. Center, USA), Willem Visser (NASA Ames Res. Center, USA)
17:30 -- 18:00
 
Abstract Matching for Software Model Checking
Pedro de la Camara, Maria del Mar Gallardo, Pedro Merino (Univ. of Malaga, ES)

Saturday April 1

  8:30 --   9:30
 
 
SPIN Invited Presentation (Chair: Antti Valmari)
Formal Verification of Industrial Microprocessor Designs
Roope Kaivola

Applications (Chair: Corina Pasareanu)
  9:30 -- 10:00
 
A Parametric State Space for the Analysis of the Infinite Class of Stop-and-Wait Protocols
Guy Edward Gallasch, Jonathan Billington (Univ. of South Australia, AU)
10:00 -- 10:30 
 
Verification of Medical Guidelines by Model Checking -- A Case Study
Simon Bäumler, Michael Balser, Andriy Dunets, Wolfgang Reif, Jonathan Schmitt (Univ. of Augsburg, D)

10:30 -- 11:00

Break

Assume--Guarantee (Chair: Markus Siegle)
11:00 -- 11:30
 
Towards a Compositional SPIN
Corina S. Pasareanu, Dimitra Giannakopoulou (NASA Ames Research Center, Moffett Field, CA, USA)

Partial Order Reduction (Chair: Markus Siegle)
11:30 -- 12:00
 
Exploiting Symmetry and Transactions for Partial Order Reduction of Rule Based Specifications
Ritwik Bhattacharya (Univ. of Utah, USA), Steven M. German (IBM T.J. Watson Research Center), Ganesh Gopalakrishnan (Univ. of Utah, USA)
12:00 -- 12:30
 
Partial-Order Reduction for General State Exploring Algorithms
Dragan Bosnacki (Eindhoven Univ. of Tech., NL), Stefan Leue (Univ. of Konstanz, D), Alberto Lluch Lafuente (Empoli, IT)

12:30 -- 14:00

Lunch


Registration to the Workshop

Via ETAPS website. Go there, click "REGISTRATION & ACCOMMODATION". The instructions seem somewhat complicated, but if you look at them, you will find that registering to SPIN only or ETAPS main conferences plus SPIN is easy.


Inquiries

Inquiries regarding the programme: spin06pc@cs.tut.fi

Inquiries regarding the local organisation: Via ETAPS website.


[Antti Valmari] April 5, 2006