Programme of SPIN at ETAPS 2006

(13th International SPIN Workshop on Model Checking of Software)

Thursday, March 30

08:30 - 09:30 SESSION 1 (SPIN, Thursday, March 30, room: EI 7)

TACAS Invited Talk
Distributed Model-Checking Algorithms for WPDS with Applications to Trust-Management Systems
Somesh Jha (Univ. of Wisconsin, Madison, USA)

09:30 - 10:00 Coffee

10:00 - 12:00 SESSION 2 (SPIN, Thursday, March 30, room: EI 7)

TACAS/SPIN Tool Demonstrations (chair: Thierry Jeron)
PRISM: A Tool for Automatic Verification of Probabilistic Systems
Andrew Hinton, Marta Kwiatkowska, Gethin Norman, and David Parker (Univ. of Birmingham, UK)
DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation
Hubert Garavel, Radu Mateescu, Damien Bergamini, Adrian Curic, Nicolas Descoubes, Christophe Joubert, Irina Smarandache-Sturm, and Gilles Stragier (INRIA Rhône-Alpes / VASY, F)
MCMAS: a Model Checker for Multi-Agent Systems
Franco Raimondi and Alessio Lomuscio (Univ. College London, UK)
A Counterexample-Guided Refinement Tool for Open Procedural Programs
Aleksandar Dimovski (Univ. of Warwick, UK), Dan R. Ghica (Univ. of Birmingham, UK), and Ranko Lazić (Univ. of Warwick, UK)

12:30 - 14:00 Lunch

14:00 - 15:00 SESSION 3a (SPIN, Thursday, March 30, room: EI 7)

FOSSACS Invited Talk
Oh Mega Completeness
Wan Fokkink (Vrije Univ. Amsterdam, NL)

15:00 - 15:15 Break

15:15 - 16:15 SESSION 3b (SPIN, Thursday, March 30, room: EI 7)

TACAS/SPIN Tool Demonstrations (chair: Susanne Graf)
jMosel: A Stand-Alone Tool and jABC Plugin for M2L(Str)
Christian Topnik, Eva Wilhelm (Univ. Dortmund, D), Tiziana Margaria (Univ. Göttingen, D), and Bernhard Steffen (Univ. Dortmund, D)
MSCan - A Tool for Analyzing MSC Specifications
Benedikt Bollig (LSV, CNRS Cachan, F), Carsten Kern, Markus Schlütter, and Volker Stolz (RWTH Aachen, D)

16:15 - 16:45 Coffee

16:45 - 18:30 SESSION 4 (SPIN, Thursday, March 30, room: EI 9)

Tool and Tutorial (chair: Dragan Bosnacki)
Model Checking Dynamic States in GROOVE
Harmen Kastenberg and Arend Rensink (Univ. of Twente, Enschede, NL)
Tutorial: Directed Model Checking
Stefan Edelkamp (Univ. of Dortmund, D)

19:30 SOCIAL EVENT (Thursday, March 30)

Intel invites all ETAPS participants to a reception in the Prechtlsaal on the ground floor of the TU Main Building, Karlsplatz 13, 1040 Wien

Friday, March 31

08:30 - 09:30 SESSION 1 (SPIN, Friday, March 31, room: EI 7)

CC Invited Talk
Using Dependent Types to Port Type Systems to Low-Level Languages
George Necula (Univ. of California, Berkeley, USA)

09:30 - 10:00 Coffee

10:00 - 12:00 SESSION 2 (SPIN, Friday, March 31, room: EI 7)

Directed Model Checking (chair: Stefan Leue)
Large-Scale Directed Model Checking LTL
Stefan Edelkamp and Shahid Jabbar (Univ. of Dortmund, D)
Directed Model Checking with Distance-Preserving Abstractions
Klaus Dräger, Bernd Finkbeiner (Univ. des Saarlandes, Saarbrücken, D), and Andreas Podelski (Max-Planck-Inst. for CS, Saarbrücken, D)
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), and Gerd Behrmann (Aalborg Univ., DK)
Larger Automata and Less Work for LTL Model Checking
Jaco Geldenhuys (Stellenbosch Univ., Matieland, RSA) and Henri Hansen (Tampere Univ. of Tech., FI)

12:30 - 14:00 Lunch

14:00 - 16:00 SESSION 3 (SPIN, Friday, March 31, room: EI 9)

Markovian Systems (chair: Gianfranco Ciardo)
Don't know in Probabilistic Systems
Harald Fecher (Univ. of Kiel, D), Martin Leucker (TU Munich, D), and Verena Wolf (Univ. of Mannheim, D)
Symbolic Model Checking of Stochastic Systems: Theory and Implementation
Matthias Kuntz and Markus Siegle (Univ. of Federal Armed Forces, Munich, D)
Distributed Model Checking (chair: Gianfranco Ciardo)
Parallel and Distributed Model Checking in Eddy
Igor Melatti, Robert Palmer, Geoffrey Sawaya, Yu Yang, Robert Mike Kirby, and Ganesh Gopalakrishnan (Univ. of Utah, USA)
Distributed On-the-Fly Model Checking and Test Case Generation
Christophe Joubert (INRIA Rhone-Alpes / VASY, F) and Radu Mateescu (ENS LYON / LIP / PLUME, F)

16:00 - 16:30 Coffee

16:30 - 18:00 SESSION 4 (SPIN, Friday, March 31, room: EI 9)

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

19:30 SOCIAL EVENT (Friday, March 31)

SPIN Dinner
Dinner at the hotel Das Triest, Wiedner Hauptstraße 12, 1040 Wien

Saturday, April 1

08:30 - 10:30 SESSION 1 (SPIN, Saturday, April 1, room: EI 9)

SPIN Invited Talk (chair: Antti Valmari)
Formal Verification of Industrial Microprocessor Designs
Roope Kaivola
Applications (chair: Corina Pasareanu)
A Parametric State Space for the Analysis of the Infinite Class of Stop-and-Wait Protocols
Guy Edward Gallasch and Jonathan Billington (Univ. of South Australia, AUS)
Verification of Medical Guidelines by Model Checking - A Case Study
Simon Bäumler, Michael Balser, Andriy Dunets, Wolfgang Reif, and Jonathan Schmitt (Univ. of Augsburg, D)

10:30 - 11:00 Coffee

11:00 - 12:30 SESSION 2 (SPIN, Saturday, April 1, room: EI 9)

Assume-Guarantee (chair: Markus Siegle)
Towards a Compositional SPIN
Corina S. Pasareanu and Dimitra Giannakopoulou (NASA Ames Research Center, Moffett Field, CA, USA)
Partial Order Reduction (chair: Markus Siegle)
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, USA), and Ganesh Gopalakrishnan (Univ. of Utah, USA)
Partial-Order Reduction for General State Exploring Algorithms
Dragan Bosnacki (Eindhoven Univ. of Tech., NL), Stefan Leue (Univ. of Konstanz, D), and Alberto Lluch Lafuente (Empoli, I)

12:30 - 14:00 Lunch

19:30 SOCIAL EVENT (Saturday, April 1)

Joint Workshops Post-Conference Dinner
Dinner at the restaurant Wiener Rathauskeller, Lanner Saal, Rathausplatz 1, 1010 Wien

Further ETAPS 2006 Programme Information:

ETAPS 2006 | Top | HTML 4.01 | Last Update: 2006-03-23