ETAPS 2006

Programme of SPIN at ETAPS 2006

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

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)

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

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)

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)

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

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

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)

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)

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)

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

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)

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)

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

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