Programme of SPIN at ETAPS 2006
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)
- Reception
- 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:
- Programme Overview
- Main Conferences:
Complete Programme,
CC,
ESOP,
FASE,
FOSSACS,
TACAS
- Workshops:
ACCAT,
AVIS,
CMCS,
COCV,
DCC,
EAAI,
FESCA,
FRCSS,
GT-VMT,
LDTA,
MBT,
QAPL,
SC,
SLAP,
TERMGRAPH,
WITS,
WRLA
- Tutorials:
Phoenix,
QuantComp
ETAPS 2006 |
Top |
HTML 4.01 |
Last Update: 2006-03-23