TACAS Programme

Programme of TACAS

MONDAY, March 29

9.00
9.30 Welcome

9.30
10.30 ESOP Invited Talk
Peter O'Hearn, Queen Mary, University of London
Resources, Concurrency and Local Reasoning
Session chair: David Schmidt

10.30
11.00 Coffee

11.00
12.30 TACAS
Theorem Proving

Session chair: Andreas Podelski

Revisiting Positive Equality
Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur (Carnegie Mellon University, USA)

An Interpolating Theorem Prover
Kenneth McMillan (Cadence, USA)

Minimal Satisfying Assignments for Bounded Model Checking
Fabio Somenzi (University of Colorado, USA), Kavita Ravi (Cadence, USA)

12.30
14.30 Lunch

14.30
16.00 TACAS
Probablistic Model Checking

Session chair: Anca Muscholl

Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study
Håkan Younes (Carnegie Mellon University, USA), Marta Kwiatkowska, Gethin Norman, David Parker (University of Birmingham, UK)

Efficient computation of time-bounded reachability probabilities in uniformized continuous-time Markov decision processes
Holger Hermanns (Universitaet des Saarlandes, D), Christel Baier (Universitaet Bonn, D), Boudewijn R. Haverkort (RWTH Aachen, D), Joost-Pieter Katoen (University of Birmingham, UK)

Model Checking Discounted Temporal Properties
Luca de Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga (University of California, Santa Cruz, USA)

16.00
16.30 Coffee

16.30
18.00 TACAS
Testing

Session chair: Ed Brinksma

Automatic Creation of Environment Models via Training
Thomas Ball, Vladimir Levin, Fei Xie (Microsoft Research, USA)

Error Explanation with Distance Metrics
Alex Groce (Carnegie Mellon University, USA)

Online Efficient Predictive Safety Analysis of Multithreaded Programs
Grigore Rosu, Koushik Sen, Gul Agha (University of Illinois at Urbana-Champaign, USA)

Evening ETAPS Reception

TUESDAY, March 30

9.00
10.00 FASE Invited Talk
Gruia-Catalin Roman(Washington University, USA)
A Formal Treatment of Context-Awareness
Session chair: Tiziana Margaria and Michel Wermelinger

10.00
10.30 Coffee

10.30
12.30 TACAS
Tools

Session chair: Bernhard Steffen

Vooduu: Verification of Object-Oriented Designs Using UPPAAL
Karsten Diethers, Michaela Huhn (Technische Universitaet Braunschweig, D)

CoPS - Checker of Persistent Security
Sabina Rossi (Università di Venezia, I), Carla Piazza, Enrico Pivato(Università di Udine, I)

Tampere Verification Tool
Henri Hansen, Heikki Virtanen, Henri Hansen, Antti Valmari, Juha Nieminen, Timo Erkkilä (Tampere University of Technology, SF)

SyncGen: An Aspect-Oriented Framework for Automatically Generating Synchronization Implementations from High-Level Specifications
John Hatcliff, Xianghua Deng, Matthew Dwyer, Masaaki Mizuno (Kansas State University, USA)

MetaGame: An Animation Tool for Model-Checking Games
Markus Müller-Olm, Haiseung Yoo (Universitaet Dortmund, D)

A Tool for Checking ANSI-C Programs
Daniel Kroening, Edmund Clarke (Carnegie Mellon University, USA), Flavio Lerda (NASA Ames Research Center, USA)

12.30
14.30 Lunch

16:30
17.00 Coffee

17.00
18.30 TACAS
Explicite State/Petri Nets

Session chair: Antti Valmari

Obtaining Memory-Efficient Reachability Graph Representations Using the Sweep-Line Method
Michael Westergaard, Thomas Mailund (University of Aarhus, DK)

Automated generation of a progress measure for the sweep-line method
Karsten Schmidt (Humboldt Universitaet Berlin, D)

Tarjan's Algorithm Makes On-the-fly LTL Verification More Efficient
Jaco Geldenhuys, Antti Valmari (Tampere University of Technology, SF)

WEDNESDAY, March 31

9.00
10.00 ETAPS Invited Talk
Serge Abiteboul (INRIA-Rocquencourt, F)
Distributed information management with XML and Web services
Session chair: José Fiadeiro

10.00
10.30 Coffee

12.30
14.30 Lunch

14.30
15.30 FOSSACS Invited Talk
Hubert Comon (École Normale Supérieure de Cachan, F)
Intruder Theories
Session chair: Igor Walukiewicz

15.30
16.30 TACAS
Scheduling

Session chair: Orna Kupferman

Resource-Optimal Scheduling Using Priced Timed Automata
Jacob Rasmussen, Kim G. Larsen (Aalborg University, DK), K. Subramani (West Virginia University , USA)

Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata
Yi Wang (Uppsala University, S), Pavel Krcal (Uppsala University, S)

16.30
17.00
Coffee

17.00
18.30 TACAS
Constraint Solving

Session chair: Giorgio Delzanno

The Succinct Solver Suite
Henrik Pilegaard, Flemming Nielson, Hanne Riis Nielson, Sun Hongyan, Mikael, René Buchholtz, Rydhof Hansen (Technical University of Denmark, DK), Helmut Seidl (TU Muenchen, D)

Binding-Time Analysis for MetaML via Type Inference and Constraint Solving
Nathan Linger, Tim Sheard (Oregon Graduate Institute, USA)

A Class of Polynomially Solvable Range Constraints for Interval Analysis without Widenings and Narrowings
Zhendong Su, David Wagner (University of California, Berkeley, USA)

Evening ETAPS DINNER

THURSDAY, April 1

9.00
10.00 TACAS Invited Talk
Antti Valmari (Tampere University of Technology, SF)
What the Small Rubik's Cube Taught Me on Data Structures, Information Theory and Randomisation
Session chair: Kurt Jensen

10.00
10.30 Coffee

10.30
12.30 TACAS
Timed Systems

Session chair: Susanna Donatelli

A Partial Order Semantics Approach to the Clock Explosion Problem of Timed Automata
Peter Niebert, Sarah Zennou, Denis Lugiez (Universite de Provence Marseille, F)

Lower and Upper Bounds in Zone Based Abstractions of Timed Automata
Gerd Behrmann (Aalborg University, DK), Patricia Bouyer (CNRS and
École Normale Supérieure de Cachan, F), Kim G. Larsen (Aalborg University, DK), Radek Pelánek (MU Brno, CZ)

A Scalable Incomplete Test for the Boundedness of UML RT Models
Stefan Leue, Richard Mayr, Wei Wei (Universitaet Freiburg, D)

Automatic Verification of Time-Sensitive Cryptographic Protocols
Giorgio Delzanno (Università di Genova, I), Pierre Ganty (Université Libre de Bruxelles, B)

12.30
14.30 Lunch

14.30
15.30 CC Invited Talk
Mary Lou Soffa (University of Pittsburgh, USA)
Developing a Foundation for Code Optimization
Session chair: Evelyn Duesterwald

15.30
16.30 TACAS
Case Studies

Session chair: John Hatcliff

Simulation-Based Verification of Autonomous Controllers with Livingstone PathFinder
Tony Lindsey, Charles Pecheur (NASA Ames Research Center, USA)

Automatic Parametric Verification of Root Contention Protocol based on Abstract State Machines and First Order Timed Logic
Daniele Beauquier, Tristan Crolard, Evguenia Prokofieva (Université Paris XII, F)

16.30
17.00 Coffee

17.00
18.30 TACAS
Software

Session chair: Cormac Flanagan

Refining approximations in software predicate abstraction
Byron Cook, Thomas Ball (Microsoft, USA), Satyaki Das (Stanford University, USA), Sriram K. Rajamani (Microsoft, USA)

Checking Strong Specifications Using An Extensible Software Model-checking Framework
Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff (Kansas State University, USA)

Applying Game Semantics to Compositional Software Modeling and Verification
Dan Ghica, Samson Abramsky, Andrzej Murawski, Luke Ong (Oxford University, UK)

Evening
eTX Reception

FRIDAY, April 2

9.00
10.00 ETAPS Invited Talk
Robin Milner (Cambridge University, UK)
A Grand Challenge: Theories for Global Ubiquitous Computing
Session chair: Fernando Orejas

10.00
10.30 Coffee

10.30
12.30 TACAS
Temporal Logic

Session chair: Kim Guldstrand Larsen

Solving disjunctive/conjunctive boolean equation systems with alternating fixed points
Misa Keinänen (Helsinki University of Technology, SF), Jan Friso Groote (Eindhoven University of Technology, NL)

How Vacuous is Vacuous?
Marsha Chechik, Arie Gurfinkel (University of Toronto, CDN)

A Temporal Logic of Nested Calls and Returns
P. Madhusudan, Rajeev Alur (University of Pennsylvania, USA), Kousha Etessami (University of Edinburgh, UK)

Liveness with Incomprehensible Ranking
Amir Pnueli (Weizmann Institute, IL), Yi Fang (New York University, USA), Nir Piterman (Weizmann Institute, IL), Lenore Zuck (New York University, USA)

12.30
14.30 Lunch

14.30
16.30 TACAS
Abstraction

Session chair: Yassine Lakhnech

Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases
Kairong Qian, Albert Nymeyer (University of New South Wales, AU)

Numerical Domains with Summarized Dimensions
Denis Gopan, Frank DiMaio (University of Wisconsin, USA), Nurit Dor (Tel-Aviv University, IL), Thomas Reps (University of Wisconsin, USA), Mooly Sagiv (Tel-Aviv University, IL)

Symbolically Computing Most-Precise Abstract Operations for Shape Analysis
Greta Yorsh (Tel-Aviv University, IL), Thomas Reps (University of Wisconsin, USA), Mooly Sagiv (Tel-Aviv University, IL)

Monotonic Abstraction-Refinement for CTL
Orna Grumberg, Sharon Shoham (Israel Institute of Technology, IL)

16.30
17.00 Coffee

17.00
18.30 TACAS
Automata Techniques

Session chair: Witold Charatonik

Omega-Regular Model Checking
Bernard Boigelot, Axel Legay, Pierre Wolper (Universite de Liege, B)

FASTer acceleration of counter automata in practice
Sebastien Bardin, Alain Finkel, Jerome Leroux (ENS Cachan, F)

From Complementation to Certification
Moshe Vardi (Rice University, USA), Orna Kupferman (Hebrew University Jerusalem, IL)

18.30
19.00 Closing

MONDAY, March 29
9.00 9.30	Welcome
9.30 10.30	ESOP Invited Talk Peter O'Hearn, Queen Mary, University of London Resources, Concurrency and Local Reasoning Session chair: David Schmidt
10.30 11.00	Coffee
11.00 12.30	TACAS Theorem Proving Session chair: Andreas Podelski Revisiting Positive Equality Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur (Carnegie Mellon University, USA) An Interpolating Theorem Prover Kenneth McMillan (Cadence, USA) Minimal Satisfying Assignments for Bounded Model Checking Fabio Somenzi (University of Colorado, USA), Kavita Ravi (Cadence, USA)
12.30 14.30	Lunch
14.30 16.00	TACAS Probablistic Model Checking Session chair: Anca Muscholl Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study Håkan Younes (Carnegie Mellon University, USA), Marta Kwiatkowska, Gethin Norman, David Parker (University of Birmingham, UK) Efficient computation of time-bounded reachability probabilities in uniformized continuous-time Markov decision processes Holger Hermanns (Universitaet des Saarlandes, D), Christel Baier (Universitaet Bonn, D), Boudewijn R. Haverkort (RWTH Aachen, D), Joost-Pieter Katoen (University of Birmingham, UK) Model Checking Discounted Temporal Properties Luca de Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga (University of California, Santa Cruz, USA)
16.00 16.30	Coffee
16.30 18.00	TACAS Testing Session chair: Ed Brinksma Automatic Creation of Environment Models via Training Thomas Ball, Vladimir Levin, Fei Xie (Microsoft Research, USA) Error Explanation with Distance Metrics Alex Groce (Carnegie Mellon University, USA) Online Efficient Predictive Safety Analysis of Multithreaded Programs Grigore Rosu, Koushik Sen, Gul Agha (University of Illinois at Urbana-Champaign, USA)
Evening	ETAPS Reception
TUESDAY, March 30
9.00 10.00	FASE Invited Talk Gruia-Catalin Roman(Washington University, USA) A Formal Treatment of Context-Awareness Session chair: Tiziana Margaria and Michel Wermelinger
10.00 10.30	Coffee
10.30 12.30	TACAS Tools Session chair: Bernhard Steffen Vooduu: Verification of Object-Oriented Designs Using UPPAAL Karsten Diethers, Michaela Huhn (Technische Universitaet Braunschweig, D) CoPS - Checker of Persistent Security Sabina Rossi (Università di Venezia, I), Carla Piazza, Enrico Pivato(Università di Udine, I) Tampere Verification Tool Henri Hansen, Heikki Virtanen, Henri Hansen, Antti Valmari, Juha Nieminen, Timo Erkkilä (Tampere University of Technology, SF) SyncGen: An Aspect-Oriented Framework for Automatically Generating Synchronization Implementations from High-Level Specifications John Hatcliff, Xianghua Deng, Matthew Dwyer, Masaaki Mizuno (Kansas State University, USA) MetaGame: An Animation Tool for Model-Checking Games Markus Müller-Olm, Haiseung Yoo (Universitaet Dortmund, D) A Tool for Checking ANSI-C Programs Daniel Kroening, Edmund Clarke (Carnegie Mellon University, USA), Flavio Lerda (NASA Ames Research Center, USA)
12.30 14.30	Lunch
16:30 17.00	Coffee
17.00 18.30	TACAS Explicite State/Petri Nets Session chair: Antti Valmari Obtaining Memory-Efficient Reachability Graph Representations Using the Sweep-Line Method Michael Westergaard, Thomas Mailund (University of Aarhus, DK) Automated generation of a progress measure for the sweep-line method Karsten Schmidt (Humboldt Universitaet Berlin, D) Tarjan's Algorithm Makes On-the-fly LTL Verification More Efficient Jaco Geldenhuys, Antti Valmari (Tampere University of Technology, SF)
WEDNESDAY, March 31
9.00 10.00	ETAPS Invited Talk Serge Abiteboul (INRIA-Rocquencourt, F) Distributed information management with XML and Web services Session chair: José Fiadeiro
10.00 10.30	Coffee
12.30 14.30	Lunch
14.30 15.30	FOSSACS Invited Talk Hubert Comon (École Normale Supérieure de Cachan, F) Intruder Theories Session chair: Igor Walukiewicz
15.30 16.30	TACAS Scheduling Session chair: Orna Kupferman Resource-Optimal Scheduling Using Priced Timed Automata Jacob Rasmussen, Kim G. Larsen (Aalborg University, DK), K. Subramani (West Virginia University , USA) Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata Yi Wang (Uppsala University, S), Pavel Krcal (Uppsala University, S)
16.30 17.00	Coffee
17.00 18.30	TACAS Constraint Solving Session chair: Giorgio Delzanno The Succinct Solver Suite Henrik Pilegaard, Flemming Nielson, Hanne Riis Nielson, Sun Hongyan, Mikael, René Buchholtz, Rydhof Hansen (Technical University of Denmark, DK), Helmut Seidl (TU Muenchen, D) Binding-Time Analysis for MetaML via Type Inference and Constraint Solving Nathan Linger, Tim Sheard (Oregon Graduate Institute, USA) A Class of Polynomially Solvable Range Constraints for Interval Analysis without Widenings and Narrowings Zhendong Su, David Wagner (University of California, Berkeley, USA)
Evening	ETAPS DINNER
THURSDAY, April 1
9.00 10.00	TACAS Invited Talk Antti Valmari (Tampere University of Technology, SF) What the Small Rubik's Cube Taught Me on Data Structures, Information Theory and Randomisation Session chair: Kurt Jensen
10.00 10.30	Coffee
10.30 12.30	TACAS Timed Systems Session chair: Susanna Donatelli A Partial Order Semantics Approach to the Clock Explosion Problem of Timed Automata Peter Niebert, Sarah Zennou, Denis Lugiez (Universite de Provence Marseille, F) Lower and Upper Bounds in Zone Based Abstractions of Timed Automata Gerd Behrmann (Aalborg University, DK), Patricia Bouyer (CNRS and École Normale Supérieure de Cachan, F), Kim G. Larsen (Aalborg University, DK), Radek Pelánek (MU Brno, CZ) A Scalable Incomplete Test for the Boundedness of UML RT Models Stefan Leue, Richard Mayr, Wei Wei (Universitaet Freiburg, D) Automatic Verification of Time-Sensitive Cryptographic Protocols Giorgio Delzanno (Università di Genova, I), Pierre Ganty (Université Libre de Bruxelles, B)
12.30 14.30	Lunch
14.30 15.30	CC Invited Talk Mary Lou Soffa (University of Pittsburgh, USA) Developing a Foundation for Code Optimization Session chair: Evelyn Duesterwald
15.30 16.30	TACAS Case Studies Session chair: John Hatcliff Simulation-Based Verification of Autonomous Controllers with Livingstone PathFinder Tony Lindsey, Charles Pecheur (NASA Ames Research Center, USA) Automatic Parametric Verification of Root Contention Protocol based on Abstract State Machines and First Order Timed Logic Daniele Beauquier, Tristan Crolard, Evguenia Prokofieva (Université Paris XII, F)
16.30 17.00	Coffee
17.00 18.30	TACAS Software Session chair: Cormac Flanagan Refining approximations in software predicate abstraction Byron Cook, Thomas Ball (Microsoft, USA), Satyaki Das (Stanford University, USA), Sriram K. Rajamani (Microsoft, USA) Checking Strong Specifications Using An Extensible Software Model-checking Framework Robby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff (Kansas State University, USA) Applying Game Semantics to Compositional Software Modeling and Verification Dan Ghica, Samson Abramsky, Andrzej Murawski, Luke Ong (Oxford University, UK)
Evening	eTX Reception
FRIDAY, April 2
9.00 10.00	ETAPS Invited Talk Robin Milner (Cambridge University, UK) A Grand Challenge: Theories for Global Ubiquitous Computing Session chair: Fernando Orejas
10.00 10.30	Coffee
10.30 12.30	TACAS Temporal Logic Session chair: Kim Guldstrand Larsen Solving disjunctive/conjunctive boolean equation systems with alternating fixed points Misa Keinänen (Helsinki University of Technology, SF), Jan Friso Groote (Eindhoven University of Technology, NL) How Vacuous is Vacuous? Marsha Chechik, Arie Gurfinkel (University of Toronto, CDN) A Temporal Logic of Nested Calls and Returns P. Madhusudan, Rajeev Alur (University of Pennsylvania, USA), Kousha Etessami (University of Edinburgh, UK) Liveness with Incomprehensible Ranking Amir Pnueli (Weizmann Institute, IL), Yi Fang (New York University, USA), Nir Piterman (Weizmann Institute, IL), Lenore Zuck (New York University, USA)
12.30 14.30	Lunch
14.30 16.30	TACAS Abstraction Session chair: Yassine Lakhnech Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases Kairong Qian, Albert Nymeyer (University of New South Wales, AU) Numerical Domains with Summarized Dimensions Denis Gopan, Frank DiMaio (University of Wisconsin, USA), Nurit Dor (Tel-Aviv University, IL), Thomas Reps (University of Wisconsin, USA), Mooly Sagiv (Tel-Aviv University, IL) Symbolically Computing Most-Precise Abstract Operations for Shape Analysis Greta Yorsh (Tel-Aviv University, IL), Thomas Reps (University of Wisconsin, USA), Mooly Sagiv (Tel-Aviv University, IL) Monotonic Abstraction-Refinement for CTL Orna Grumberg, Sharon Shoham (Israel Institute of Technology, IL)
16.30 17.00	Coffee
17.00 18.30	TACAS Automata Techniques Session chair: Witold Charatonik Omega-Regular Model Checking Bernard Boigelot, Axel Legay, Pierre Wolper (Universite de Liege, B) FASTer acceleration of counter automata in practice Sebastien Bardin, Alain Finkel, Jerome Leroux (ENS Cachan, F) From Complementation to Certification Moshe Vardi (Rice University, USA), Orna Kupferman (Hebrew University Jerusalem, IL)
18.30 19.00	Closing