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