PROGRAMME OF TACAS

Programme of TACAS

MONDAY, 8 April

9.00
9.30 Welcome

9.30
10.30 FASE Invited Talk
Hellmuth Broda (Sun Microsystems (Schweiz) AG)
Jini Software Architecture - The End of Protocols as we know them
Session chair: Herbert Weber

10.30
11.15 Coffee

11.15
12.45 TACAS
Real-time and probabilistic systems

Session chair: Joost-Pieter Katoen

Improving the Verification of Timed Systems using Influence Information
Victor Braberman, Diego Garbervetsky, Alfredo Olivero (Universidad de Buenos Aires & Universidad Argentina de la Empresa)
Digitisation and Full Abstraction for Dense-Time Model Checking
Joel Ouaknine (Tulane University, USA)
Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach
Marta Kwiatkowska, Gethin Norman, David Parker (U. Birmingham, UK)

12.45
14.15 Lunch

14.15
16.15 TACAS
Scheduling

Session chair: Kim G. Larsen

Timed Automata with Asynchronous Processes: Schedulability and Decidability
Elena Fersman, Paul Pettersson, Wang Yi (Uppsala Univ., Sweden)
Validating Timing Constraints of Dependent Jobs with Variable Execution Times in Distributed Real-Time Systems
Hojung Cha, Rhan Ha (Hongik Univ. & Yonsei Univ., S Korea)
An Analysis of Zero-Clairvoyant Scheduling
K. Subramani (West Virginia Univ., USA)
Preemptive Job-Shop Scheduling using Stopwatch Automata
Yasmina Abdeddaim, Oded Maler (VERIMAG, Grenoble, F)

16.15
16.45 Coffee

16.45
18.15 TACAS
Miscellaneous

Session chair: Hubert Garavel

Explicit Modeling of Influences, and of Their Absence, in Distributed Systems
Horst F. Wedde, Arnim Wedig (Univ. Dortmund, D)
A Functional Semantics of Attribute Grammars
Kevin Backhouse (Oxford Univ., UK)
TIMES - A Tool for Modelling and Implementation of Embedded Systems
Tobias Amnell, Elena Fersman, Leonid Mokrushin, Paul Petterson, Wang Yi (Uppsala Univ., Sweden)

20.00 Reception

TUESDAY, 9 April

9.00
10.00 ESOP Invited Talk
Greg Morrisett (Cornell University, USA)
Type Checking Systems Code
Session chair: Daniel Le Métayer

10.00
10.45 Coffee

10.45
12.45 TACAS
Software verification

Session chair: Wang Yi

Relative Completeness of Abstraction Refinement for Software Model Checking
Thomas Ball, Andreas Podelski, Sriram K. Rajamani (Microsoft Research, USA & Max-Planck Institute, D)
Towards the Automated Verification of Multithreaded Java Programs
Giorgio Delzanno, Jean-Francois Raskin, Laurent Van Begin (Universitá di Genova, I & Université Libre de Bruxelles, B)
CLPS-B - A Constraint Solver for B
F. Bouquet, Bruno Legeard, Fabien Peureux (Laboratoire d'Informatique Université de Franche-Comté, F)
Formal Verification of Functional Properties of an SCR-style Software Requirements Specification using PVS
Taeho Kim, David Stringer-Calvert, Sungdeok Cha (KAIST, S Korea & SRI Int., USA)

12.45
14.15 Lunch

14.15
15.15 TACAS Invited Talk
Michael Lowry (NASA Ames Research Center)
Software Construction and Analysis Tools for Future Space Missions
Session chair: Perdita Stevens

15.15
16.00 Coffee

16.00
17.30 TACAS
Infinite-state and parametric systems

Session chair: Bernard Steffen

Beyond Parameterized Verification
Marco Bozzano, Giorgio Delzanno (Univ. Genova, I)
Resource-Constrained Model Checking of Recursive Programs
Samik Basu, K. Narayan Kumar, L. Robert Pokorny, C. R. Ramakrishnan (State University New York, USA & Chennai Mathematical Inst., India)
Model Checking Large-scale and Parameterized Resource Allocation Systems
Allen Emerson, Vineet Kahlon (Univ. of Texas at Austin, USA)

17.30
17.45 Short Break

17.45
18.45 TACAS
Tool demo

Session chair: Joost-Pieter Katoen

Compositional Verification using SVL Scripts
Frédéric Lang (INRIA Rhône-Alpes, F)

20.00 nyd

WEDNESDAY, 10 April

9.00
10.00 ETAPS Invited Talk
Daniel Jackson (MIT Lab for Computer Science)
Alloy: A New Technology for Software Modelling
Session chair: Susanne Graf

10.00
10.45 Coffee

10.45
12.45 TACAS
Model checking: logics and algorithms

Session chair: John Hatcliff

Exploring Very Large State Spaces Using Genetic Algorithms
Patrice Godefroid, Sarfraz Khurshid (Bell Labs & MIT, USA)
Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems
Radu Mateescu (INRIA Rhône-Alpes, F)
The ForSpec Temporal Logic: A New Temporal Property-Specification Language
R. Armoni, L. Fix, A. Flaisher, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador-Haim, E. Singerman, A. Tiemeyer, M.Y. Vardi, Y. Zbar (Rice University, USA, & Intel, USA/Israel)
Fine-Grained Conjunction Scheduling for Symbolic Reachablity Analysis
HoonSang Jin, Andreas Kuehlmann, Fabio Somenzi (Univ. of Colorado, Boulder & Cadence Berkeley Labs, USA)

12.45
14.15 Lunch

14.15
15.15 ETAPS Invited Talk
Mary Shaw (Carnegie Mellon University)
What Makes Good Research in Software Engineering?
Session chair: José Fiadeiro

15.15
16.00 Coffee

16.00
17.30 TACAS
Model checking and testing (3)

Session chair: Ed Brinksma

A Temporal Logic Based Theory of Test Coverage and Generation
Hyoung Seok Hong, Insup Lee, Oleg Sokolsky, Hasan Ural (Univ. Pennsylvania, USA & University of Ottawa, Canada)
Synthesizing Monitors for Safety Properties
Klaus Havelund, Grigore Rosu (NASA Ames Research Center, USA)
Adaptive Model Checking
Alex Groce, Doron Peled, Mihalis Yannakakis (Carnegie Mellon Univ., USA, Univ. of Texas, Austin, & Avaya Laboratories, USA)

17.30
17.45 Short break

17.45
18.45 TACAS
Tool demo (1 of 2)

Session chair: Matthew Dwyer

STG: A Symbolic Test Generation Tool
Duncan Clarke, Thierry Jéron, Vlad Rusu, Elena Zinovieva (IRISA/INRIA Rennes, F)

20.00 ETAPS DINNER

THURSDAY, 11 April

9.00
10.00 FOSSACS Invited Talk
Bruno Courcelle (Université Bordeaux, F)
Semantical Evaluations as Monadic Second-order Compatible Structure Transformations
Session chair: Mogens Nielsen

10.00
10.45 Coffee

10.45
12.45 TACAS
Partial-order and simulation techniques

Session chair: Claude Jard

Parallelisation of the Petri Net Unfolding Algorithm
Keijo Heljanko, Victor Khomenko, Maciej Koutny (Helsinki Univ. of Technology, Finland & Univ. of Newcastle, UK)
Black Box Unfolding with Local First Search
Sebastien Bornot, Remi Morin, Peter Niebert, Sarah Zennou (Laboratoire d'Informatique Fondamentale de Marseille, F)
Applicability of Fair Simulation
Doran Bustan, Orna Grumberg (Technion Haifa, Israel)
Simulation as Coarsest Partition Problem
Raffaella Gentilini, Carla Piazza, Alberto Policriti (Univ. Udine, I)

12.45
14.15 Lunch

14.15
15.15 SPIN Invited Talk
Ed Clarke (Carnegie Mellon University)
SAT-based Counterexample Guided Abstraction Refinement
Session chair:

15.15
16.00 Coffee

16.00
17.30 TACAS
Debugging with model checking

Session chair: Perdita Stevens

Temporal Debugging for Concurrent Systems
Elsa Gunter, Doron Peled (New Jersey Inst. of Science & Univ. of Texas, Austin, USA)
Fate and Free Will in Error Traces
HoonSang Jin, Kavita Ravi, Fabio Somenzi (Univ. of Colorado, Boulder & Cadence Design Systems, USA)
Real-Time Systems Design with PEP
Christian Stehno (Univ. Oldenburg, D)

MONDAY, 8 April
9.00 9.30	Welcome
9.30 10.30	FASE Invited Talk Hellmuth Broda (Sun Microsystems (Schweiz) AG) Jini Software Architecture - The End of Protocols as we know them Session chair: Herbert Weber
10.30 11.15	Coffee
11.15 12.45	TACAS Real-time and probabilistic systems Session chair: Joost-Pieter Katoen Improving the Verification of Timed Systems using Influence Information Victor Braberman, Diego Garbervetsky, Alfredo Olivero (Universidad de Buenos Aires & Universidad Argentina de la Empresa) Digitisation and Full Abstraction for Dense-Time Model Checking Joel Ouaknine (Tulane University, USA) Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach Marta Kwiatkowska, Gethin Norman, David Parker (U. Birmingham, UK)
12.45 14.15	Lunch
14.15 16.15	TACAS Scheduling Session chair: Kim G. Larsen Timed Automata with Asynchronous Processes: Schedulability and Decidability Elena Fersman, Paul Pettersson, Wang Yi (Uppsala Univ., Sweden) Validating Timing Constraints of Dependent Jobs with Variable Execution Times in Distributed Real-Time Systems Hojung Cha, Rhan Ha (Hongik Univ. & Yonsei Univ., S Korea) An Analysis of Zero-Clairvoyant Scheduling K. Subramani (West Virginia Univ., USA) Preemptive Job-Shop Scheduling using Stopwatch Automata Yasmina Abdeddaim, Oded Maler (VERIMAG, Grenoble, F)
16.15 16.45	Coffee
16.45 18.15	TACAS Miscellaneous Session chair: Hubert Garavel Explicit Modeling of Influences, and of Their Absence, in Distributed Systems Horst F. Wedde, Arnim Wedig (Univ. Dortmund, D) A Functional Semantics of Attribute Grammars Kevin Backhouse (Oxford Univ., UK) TIMES - A Tool for Modelling and Implementation of Embedded Systems Tobias Amnell, Elena Fersman, Leonid Mokrushin, Paul Petterson, Wang Yi (Uppsala Univ., Sweden)
20.00	Reception
TUESDAY, 9 April
9.00 10.00	ESOP Invited Talk Greg Morrisett (Cornell University, USA) Type Checking Systems Code Session chair: Daniel Le Métayer
10.00 10.45	Coffee
10.45 12.45	TACAS Software verification Session chair: Wang Yi Relative Completeness of Abstraction Refinement for Software Model Checking Thomas Ball, Andreas Podelski, Sriram K. Rajamani (Microsoft Research, USA & Max-Planck Institute, D) Towards the Automated Verification of Multithreaded Java Programs Giorgio Delzanno, Jean-Francois Raskin, Laurent Van Begin (Universitá di Genova, I & Université Libre de Bruxelles, B) CLPS-B - A Constraint Solver for B F. Bouquet, Bruno Legeard, Fabien Peureux (Laboratoire d'Informatique Université de Franche-Comté, F) Formal Verification of Functional Properties of an SCR-style Software Requirements Specification using PVS Taeho Kim, David Stringer-Calvert, Sungdeok Cha (KAIST, S Korea & SRI Int., USA)
12.45 14.15	Lunch
14.15 15.15	TACAS Invited Talk Michael Lowry (NASA Ames Research Center) Software Construction and Analysis Tools for Future Space Missions Session chair: Perdita Stevens
15.15 16.00	Coffee
16.00 17.30	TACAS Infinite-state and parametric systems Session chair: Bernard Steffen Beyond Parameterized Verification Marco Bozzano, Giorgio Delzanno (Univ. Genova, I) Resource-Constrained Model Checking of Recursive Programs Samik Basu, K. Narayan Kumar, L. Robert Pokorny, C. R. Ramakrishnan (State University New York, USA & Chennai Mathematical Inst., India) Model Checking Large-scale and Parameterized Resource Allocation Systems Allen Emerson, Vineet Kahlon (Univ. of Texas at Austin, USA)
17.30 17.45	Short Break
17.45 18.45	TACAS Tool demo Session chair: Joost-Pieter Katoen Compositional Verification using SVL Scripts Frédéric Lang (INRIA Rhône-Alpes, F)
20.00	nyd
WEDNESDAY, 10 April
9.00 10.00	ETAPS Invited Talk Daniel Jackson (MIT Lab for Computer Science) Alloy: A New Technology for Software Modelling Session chair: Susanne Graf
10.00 10.45	Coffee
10.45 12.45	TACAS Model checking: logics and algorithms Session chair: John Hatcliff Exploring Very Large State Spaces Using Genetic Algorithms Patrice Godefroid, Sarfraz Khurshid (Bell Labs & MIT, USA) Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems Radu Mateescu (INRIA Rhône-Alpes, F) The ForSpec Temporal Logic: A New Temporal Property-Specification Language R. Armoni, L. Fix, A. Flaisher, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador-Haim, E. Singerman, A. Tiemeyer, M.Y. Vardi, Y. Zbar (Rice University, USA, & Intel, USA/Israel) Fine-Grained Conjunction Scheduling for Symbolic Reachablity Analysis HoonSang Jin, Andreas Kuehlmann, Fabio Somenzi (Univ. of Colorado, Boulder & Cadence Berkeley Labs, USA)
12.45 14.15	Lunch
14.15 15.15	ETAPS Invited Talk Mary Shaw (Carnegie Mellon University) What Makes Good Research in Software Engineering? Session chair: José Fiadeiro
15.15 16.00	Coffee
16.00 17.30	TACAS Model checking and testing (3) Session chair: Ed Brinksma A Temporal Logic Based Theory of Test Coverage and Generation Hyoung Seok Hong, Insup Lee, Oleg Sokolsky, Hasan Ural (Univ. Pennsylvania, USA & University of Ottawa, Canada) Synthesizing Monitors for Safety Properties Klaus Havelund, Grigore Rosu (NASA Ames Research Center, USA) Adaptive Model Checking Alex Groce, Doron Peled, Mihalis Yannakakis (Carnegie Mellon Univ., USA, Univ. of Texas, Austin, & Avaya Laboratories, USA)
17.30 17.45	Short break
17.45 18.45	TACAS Tool demo (1 of 2) Session chair: Matthew Dwyer STG: A Symbolic Test Generation Tool Duncan Clarke, Thierry Jéron, Vlad Rusu, Elena Zinovieva (IRISA/INRIA Rennes, F)
20.00	ETAPS DINNER
THURSDAY, 11 April
9.00 10.00	FOSSACS Invited Talk Bruno Courcelle (Université Bordeaux, F) Semantical Evaluations as Monadic Second-order Compatible Structure Transformations Session chair: Mogens Nielsen
10.00 10.45	Coffee
10.45 12.45	TACAS Partial-order and simulation techniques Session chair: Claude Jard Parallelisation of the Petri Net Unfolding Algorithm Keijo Heljanko, Victor Khomenko, Maciej Koutny (Helsinki Univ. of Technology, Finland & Univ. of Newcastle, UK) Black Box Unfolding with Local First Search Sebastien Bornot, Remi Morin, Peter Niebert, Sarah Zennou (Laboratoire d'Informatique Fondamentale de Marseille, F) Applicability of Fair Simulation Doran Bustan, Orna Grumberg (Technion Haifa, Israel) Simulation as Coarsest Partition Problem Raffaella Gentilini, Carla Piazza, Alberto Policriti (Univ. Udine, I)
12.45 14.15	Lunch
14.15 15.15	SPIN Invited Talk Ed Clarke (Carnegie Mellon University) SAT-based Counterexample Guided Abstraction Refinement Session chair:
15.15 16.00	Coffee
16.00 17.30	TACAS Debugging with model checking Session chair: Perdita Stevens Temporal Debugging for Concurrent Systems Elsa Gunter, Doron Peled (New Jersey Inst. of Science & Univ. of Texas, Austin, USA) Fate and Free Will in Error Traces HoonSang Jin, Kavita Ravi, Fabio Somenzi (Univ. of Colorado, Boulder & Cadence Design Systems, USA) Real-Time Systems Design with PEP Christian Stehno (Univ. Oldenburg, D)