TACAS 2009

Fifteenth International Conference on
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION
AND ANALYSIS OF SYSTEMS

A member conference of the European Joint Conferences
on Theory and Practice of Software
(ETAPS 2009)

22 - 29 March, 2009, York, UK

News (16 March 2009): The corrected program is now available.

CONFERENCE DESCRIPTION

TACAS is a forum for researchers, developers and users interested in rigorously based tools and algorithms for the construction and analysis of systems. The conference serves to bridge the gaps between different communities that share common interests in, and techniques for, tool development and its algorithmic foundations. The research areas covered by such communities include but are not limited to formal methods, software and hardware verification, static analysis, programming languages, software engineering, real-time systems, communications protocols, and biological systems. The TACAS forum provides a venue for such communities at which common problems, heuristics, algorithms, data structures and methodologies can be discussed and explored. In doing so, TACAS aims to support researchers in their quest to improve the utility, reliability, flexibility and efficiency of tools and algorithms for building systems.

TACAS is a member conference of the European Joint Conferences on Theory and Practice of Software (ETAPS), which is the primary European forum for academic and industrial researchers working on topics relating to Software Science. ETAPS 2009 is the twelfth joint conference in this series. The prior conferences have been ETAPS 1998 in Lisbon, ETAPS 1999 in Amsterdam, ETAPS 2000 in Berlin, ETAPS 2001 in Genova, ETAPS 2002 in Grenoble, ETAPS 2003 in Warsaw, ETAPS 2004 in Barcelona, ETAPS 2005 in Edinburgh, ETAPS 2006 in Vienna, ETAPS 2007 in Braga, and ETAPS 2008 in Budapest.

CALL FOR PAPERS

Tool descriptions and case studies with a conceptual message, as well as theoretical papers with clear relevance for tool construction are all encouraged. The specific topics covered by the conference include, but are not limited to, the following:

· Specification and verification techniques for finite and infinite-state systems

· Software and hardware verification

· Theorem-proving and model-checking

· System construction and transformation techniques

· Static and run-time analysis

· Abstraction techniques for modeling and validation

· Compositional and refinement-based methodologies

· Testing and test-case generation

· Analytical techniques for secure, real-time, hybrid, critical, biological or dependable systems

· Integration of formal methods and static analysis in high-level hardware design or software environments

· Tool environments and tool architectures

· SAT solvers

· Applications and case studies

As TACAS addresses a heterogeneous audience, potential authors are strongly encouraged to write about their ideas and findings in general and jargon-independent, rather than in application- and domain-specific, terms. Authors reporting on tools or case studies are strongly encouraged to indicate how their experimental results can be reproduced and confirmed independently.

The list of accepted papers is available here.

IMPORTANT DATES

ETAPS 2009 conferences and other satellite events will be held 22 - 29 March, 2009.

As a part of ETAPS, TACAS adheres to ETAPS submission and notification deadlines:

· 2 October, 2008	Deadline for submission of abstracts (strict)
· 9 October, 2008	Deadline for submission of full versions (strict)
· 12 December, 2008	Notification of acceptance / rejection
· 5 January, 2009	Camera-ready paper versions due (strict)
· 22 - 29 March 2009	TACAS 2009 Conference

The above deadlines are STRICT. Making the deadline for submission of abstracts a week early allows the programme committee to start work before full versions are available. Obviously, there is no need to wait with submission of the full version until the final deadline.

Submission of an abstract implies no obligation to submit a full version; abstracts with no corresponding full versions by the final deadline will be treated as withdrawn, but authors are strongly encouraged, in this case, to explicitly withdraw their submission by sending an e-mail to the chairpersons.

SUBMISSION GUIDELINES

Papers should be submitted using the TACAS 2009 Conference Service.

As with other ETAPS conferences, TACAS accepts two types of contributions: research papers and tool demonstration papers. Both types of contributions will appear in the proceedings and have oral presentations during the conference.

Research papers

Research papers cover one or more of the topics above, including tool development and case studies from a perspective of scientific research. Research papers are evaluated by the TACAS Program Committee. Research papers may contain an appendix with ancillary material (e.g. proofs) or a reference to a webpage but referees will decide whether or not to look at such material or webpages. Submitted research papers must:

· be in English and have a maximum of 15 pages (including figures and bibliography; but excluding an optional appendix or URL containing ancillary material such as proofs, both at the discretion of referees),

· present original research which is unpublished and not submitted elsewhere (conferences or journals) -- in particular, simultaneous submission of the same contribution to multiple ETAPS conferences is forbidden,

· use the Springer-Verlag LNCS style

· be submitted electronically in Postscript or PDF form via the TACAS 2009 Conference Service before the deadlines stated above.

Submissions deviating from these instructions may be rejected without review. Any questions regarding this policy should be directed to the Program Committee Co-Chairs Stefan Kowalewski or Anna Philippou prior to submitting.

Tool demonstration papers

Tool demonstration papers present tools based on aforementioned technologies (e.g., theorem-proving, model-checking, static analysis, or other formal methods) or fall into the above application areas (e.g., system construction and transformation, testing, analysis of real-time, hybrid or biological systems, etc.). Submitted tool demonstration papers must:

· be in English and have a maximum of 4 pages,

· have an appendix (not included in the 4 page count) that provides a detailed description of:

o how the oral presentation will be conducted, e.g. illustrated by a number of snapshots,

o the availability of the tool, the number and types of users, other information which may illustrate the maturity and robustness of the tool,

o if applicable, a link to a web-page for the tool

(The appendix will not be included in the proceedings, but during the evaluation of the tool demonstration papers it will be equally important as the pages submitted for publication in the proceedings.)

· use the Springer-Verlag LNCS style

· clearly describe the enhancements and novel features of the tool in case that one of its previous versions has already been presented at meetings or published in some form

· be submitted electronically in Postscript or PDF form via the TACAS 2009 Conference Service before the deadlines stated above.

Submissions deviating from these instructions may be rejected without review. Any questions regarding this policy should be sent to the Program Chairs.

PROGRAMME COMMITTEE CO-CHAIRS

· Stefan Kowalewski, RWTH Aachen University, Aachen (Germany)

· Anna Philippou, University of Cyprus (Cyprus)

INVITED SPEAKER

· Steven Miller, Rockwell Collins (USA)

PROGRAMME COMMITTEE

· Marco Bernardo, University of Urbino (Italy)

· Ahmed Bouajjani, University of Paris 7 (France)

· Ed Brinksma, ESI and University of Twente (The Netherlands)

· Alessandro Cimatti, FBK-irst (Italy)

· Rance Cleaveland, University of Maryland & Fraunhofer USA Inc (USA)

· Swarat Chaudhuri, Pennsylvania State University (USA)

· Veronique Cortier, CNRS-LORIA, Nancy (France)

· Patrice Godefroid, Microsoft Research, Redmond, Washington (USA)

· Orna Grumberg, Technion, Israel Institute of Technology (Israel)

· Aarti Gupta, NEC Laboratories America Inc, Princeton (USA)

· Nicolas Halbwachs, Verimag/CNRS, Grenoble (France)

· Michael Huth, Imperial College (UK)

· Kim Larsen, Aalborg University (Denmark)

· Stefan Kowalewski (CO-CHAIR), RWTH Aachen (Germany)

· Thomas Kropf, Robert Bosch AG (Germany)

· Marta Kwiatkowska, University of Oxford (UK)

· Rupak Majumdar, University of California (USA)

· Panagiotis Manolios, Northeastern University (USA)

· Radu Mateescu, INRIA/VASY (France)

· Ken McMillan, Cadence Berkeley Labs (USA)

· Anna Philippou (CO-CHAIR), University of Cyprus (Cyprus)

· Andreas Podelski, University of Freiburg (Germany)

· C.R. Ramakrishnan, Stony Brook University (USA)

· Natasha Sharygina, University of Lugano (Switzerland)

· Oleg Sokolsky, University of Pennsylvania (USA)

· Bernhard Steffen, University of Dortmund (Germany)

· Frits Vaandrager, Nijmegen University (The Netherlands)

· Carsten Weise, RWTH Aachen (Germany)

· Lenore Zuck, University of Illinois (USA)

TACAS STEERING COMMITTEE

Ed Brinksma, ESI and Univ. of Twente (The Netherlands)
Rance Cleaveland, University of Maryland & Fraunhofer USA Inc (USA)
Kim Larsen, Aalborg Univ. (Denmark)
Bernhard Steffen, Univ. of Dortmund (Germany)
Lenore Zuck , Univ. of Illinois (USA)

PROGRAM

Model Checking I – Session Chair: Luca de Alfaro

Hierachical Set Decision Diagrams and Regular Models.

Yann Thierry-Mieg (Universit\'{e} P. & M. Curie)

Denis Poitrenaud (Universit\'{e} P. & M. Curie)

Alexandre Hamez (Universit\'{e} P. & M. Curie)

Fabrice Kordon (Universit\'{e} P. & M. Curie)

Buchi Complementation and Size-Change Termination.

Seth Fogarty (Rice University)

Moshe Vardi (Rice University)

Learning Minimal Separating DFA's for Compositional Verification.

Yu-Fang Chen (National Taiwan University)

Azadeh Farzan (University of Toronto)

Edmund Clarke (Carnegie Mellon University)

Yih-Kuen Tsay (National Taiwan University)

Bow-Yaw Wang (Academia Sinica)

Tools I – Session Chair: Carsten Weise

RBAC-PAT: A Policy Analysis Tool for Role Based Access Control.

Mikhail Gofman (Binghampton University)

Ruiqi Luo (Binghampton University)

Ayla Solomon (Wellesley College)

Yingbin Zhang (Binghampton University)

Ping Yang (Binghampton University)

Scott Stoller (Stony Brook University)

ITPN-PerfBound: A performance bound tool for Interval Time Petri Nets.

Elina Rocio Pacini (Universit\`{a} di Torino)

Simona Bernardi (Universit\`{a} di Torino)

Marco Gribaudo (Universit\`{a} di Torino)

Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches.

Louis-Marie Traonouez (IRCCyN, CNRS)

Didier Lime (IRCCyN, CNRS)

Olivier (H.) Roux (IRCCyN, CNRS)

Charlotte Seidner (IRCCyN, CNRS)

Alpaga: A Tool for Solving Parity Games with Imperfect Information.

Dietmar Berwanger (LSV, ENS Cachan and CNRS)

Krishnendu Chatterjee (CE, University of California, Santa Cruise)

Martin De Wulf (Universit\’{e} Libre de Bruxelles)

Laurent Doyen (\’{E}cole Polytechnique F(\’{e}d(\’{e}rale de Lausanne)

Thomas A. Henzinger (\’{E}cole Polytechnique F(\’{e}d(\’{e}rale de Lausanne)

Game-theoretic Approaches – Session Chair: Michael Huth

Compositional Predicate Abstraction from Game Semantics.

Dan Ghica (University of Birmingham)

Adam Bakewell (University of Birmingham)

Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications.

Hillel Kugler (Microsoft Research, Cambridge)

Itai Segall (Weizmann Institute of Science)

Computing Weakest Strategies for Safety Games of Imperfect Information.

Wouter Kuijper (University of Twernte)

Jaco Pol (University of Twernte)

TUESDAY

Verification of Concurrent Programs - Session Chair: Natasha Sharygina

Context-bounded analysis for concurrent programs with dynamic creation of threads.

Mohamed Faouzi Atig (Liafa, CNRS and University Paris Diderot)

Ahmed Bouajjani (Liafa, CNRS and University Paris Diderot)

Shaz Qadeer (Microsoft Research, Redmond)

Semantic Reduction of Thread Interleavings for Concurrent Programs.

Vineet Kahlon (NEC Laboratories)

Sriram Sankaranarayanan (NEC Laboratories)

Aarti Gupta (NEC Laboratories)

Inferring Synchronization under Limited Observability.

Martin Vechev (IBM Research)

Eran Yahav (IBM Research)

Greta Yorsh (IBM Research)

The Complexity of Predicting Atomicity Violations.

Azadeh Farzan (University of Toronto)

Madhusudan Parthasarathy (University of Illinois at Urbana Champaign)

Tools II - Session Chair: Panayiotis Manolios

MoonWalker: verification of .NET programs.

Theo Ruys (RWTH Aachen University)

Niels H.M. Aan de Brugh (RWTH Aachen University)

Viet Yen Nguyen (RWTH Aachen University)

Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays.

Robert Daniel Brummayer (Johan Kepler University Linz)

Armin Biere (Johan Kepler University Linz)

The Yogi Project: Software Property Checking via Static Analysis and Testing.

Aditya Nori (Microsoft Research India)

Sriram Rajamani (Microsoft Research India)

Saideep Tetali (Microsoft Research India)

Aditya Thakur (University of Wisconsin-Madison)

TaPAS : The Talence Presburger Arithmetic Suite.

J\´{e}r\^{o}me Leroux (LaBRI, CNRS)

G\´{e}rald Point (LaBRI, CNRS)

Model Checking II – Session Chair: Rajeev Alur

Transition-based Directed Model Checking.

Sebastian Kupferschmid (University of Freiburg)

Martin Wehrle (University of Freiburg)

Andreas Podelski (University of Freiburg)

Memoised Garbage Collection for Software Model Checking.

Viet Yen Nguyen (RWTH Aachen University)

Theo Ruys (RWTH Aachen University)

Hierarchical Adaptive State Space Caching based on Level Sampling.

Radu Mateescu (INRIA / VASY)

Anton Wijs (INRIA / VASY)

WEDNESDAY

Parametric Analysis – Session Chair: Parosh Abdullah

Static Analysis Techniques for Parameterised Boolean Equation Systems.

Simona Orzan (Eindhoven University of Technology)

Wieger Wesselink (Eindhoven University of Technology)

Tim Willemse (Eindhoven University of Technology)

Parametric Trace Slicing and Monitoring.

Feng Chen (University of Illinois at Urbana-Champaign)

Grigore Rosu (University of Illinois at Urbana-Champaign)

Generative Approaches– Session Chair: Gerald Luettgen

An Efficient Invariant Generator.

Ashutosh Gupta (MPI-SWS)

Rupak Majumdar (University of California, Los Angeles)

Andrei Rybalchenko (MPI-SWS)

Test input generation for programs with pointers.

Dries Vanoverberghe (Katholieke Universiteit Leuven)

Nikolai Tillmann (Microsoft Research, Redmond)

Piessens, Frank (Katholieke Universiteit Leuven)

Specification Mining With Few False Positives.

Claire Le Goues (University of Virginia)

Westley Weimer (University of Virginia)

THURSDAY

Program Analysis – Session Chair: Nicholas Halbwach

Path Feasibility Analysis for String-Manipulating Programs.

Nikolaj Bj{\o}rner (Microsoft Research)

Nikolai Tillmann (Microsoft Research)

Andrei Voronkov (University of Machester)

Symbolic String Verification: Combining String Analysis and Size Analysis.

Fang Yu (University of California, Santa Barbara)

Tevfik Bultan (University of California, Santa Barbara)

Oscar H.Ibarra (University of California, Santa Barbara)

Iterating Octagons.

Marius Bozga (Verimag/CNRS)

Godru\c{t}a G\^{i}rlea (Verimag/CNRS)

Radu Iosif (Verimag/CNRS)

Verifying Reference Counting Implementation.

Michael Emmi (University of California, Los Angeles)

Ranjit Jhala (University of Calufornia, San Diego)

Eddie Kohler (University of California, Los Angeles)

Rupak Majumdar (University of California, Los Angeles)

Hybrid Systems – Session Chair Stefan Kowalewski

Falsification of LTL Safety Properties in Hybrid Systems.

Erion Plaku (Rice University)

Lydia Kavraki (Rice University)

Moshe Vardi (Rice University)

Computing Optimized Representations for Non-Convex Polyhedra by Detection and Removal of Redundant Linear Constraints.

Christoph Scholl (Albert-Ludwigs-Universit\”{a}t Freiburg)

Stefan Disch (Albert-Ludwigs-Universit\”{a}t Freiburg)

Florian Pigorsch (Albert-Ludwigs-Universit\”{a}t Freiburg)

Stefan Kupferschmid (Albert-Ludwigs-Universit\”{a}t Freiburg)

Decision Procedures and Theorem Proving: – Session Chair: Alessandro Cimatti

All-Termination(T).

Panagiotis Manolios (Northeastern University)

Aaron Turon (Northeastern University)

Ground Interpolation for the Theory of Equality.

Alexander Fuchs (University of Iowa)

Amit Goel (Intel Corporation)

Jim Grundy (Intel Corporation)

Sava Krstic (Intel Corporation)

Cesare Tinelli (University of Iowa)

Satisfiability Procedures for Combination of Theories Sharing Integer Offsets

Enrica Nicolini (LORIA and INRIA Nancy Grand Est)

Christophe Ringeissen (LORIA and INRIA Nancy Grand Est)

Michael Rusinowitch (LORIA and INRIA Nancy Grand Est)