Seventeenth International Conference on

Saarbrücken, Germany, March 26 - April 3, 2011

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 2011 is the fourteenth 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 Minho, ETAPS 2008 in Budapest, ETAPS 2009 in York, and ETAPS 2010 in Paphos.

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:

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.

Submission Guidelines

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.

Submission site is now open:

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:

Submissions deviating from these instructions may be rejected without review. Any questions regarding this policy should be directed to the Program Committee Co-Chairs, Parosh Abdulla and Rustan Leino, 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.). Tool demonstration papers are evaluated by the TACAS Tool Chair with the help of the Programme Committee. Submitted tool demonstration papers must:

Submissions deviating from these instructions may be rejected without review. Any questions regarding this policy should be directed to the Tool Chair, Alessandro Cimatti.

Important Dates

ETAPS 2011 conferences and other satellite events will be held from March 26 to April 3, 2011.

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

4 October 2010 (23:59 Samoa time) Submission of abstracts
8 October 2010 (23:59 Samoa time) Submission of full versions
10 December 2010 Notification of acceptance
3 January 2011 Camera-ready paper versions due
26 March - 3 April 2011 TACAS 2011 conference

The paper submission deadline is strict.  Making the deadline for submission of abstracts a week early allows the program committee to start work before full versions are available.  Of course, 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 e-mail to the chairs.

Accepted Papers

Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
Yungbum Jung, Wonchan Lee, Bow-Yaw Wang, and Kwangkeun Yi
Optimal Base Encodings for Pseudo-Boolean Constraints
Michael Codish, Yoav Fekete, Carsten Fuhs, and Peter Schneider-Kamp
GAVS+: An Open Platform for the Research of Algorithmic Game Solving
Chih-Hong Cheng, Alois Knoll, Christian Buckl, and Michael Luttenberger
Next Generation Learnlib
Maik Merten, Bernhard Steffen, Falk Howar, and Tiziana Margaria
Abstractions and Pattern Databases: The Quest for Succinctness and Accuracy
Sebastian Kupferschmid and Martin Wehrle
Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models
Jacob Burnim, Koushik Sen, and Christos Stergiou
Büchi Store: An Open Repository of Büchi Automata
Yih-Kuen Tsay, Ming-Hsien Tsai, Jinn-Shu Chang, and Yi-Wen Chang
Canonized rewriting and Ground AC-Completion Modulo Shostak Theories
Sylvain Conchon, Evelyne Contejean, and Mohamed Iguernelala
Off-line Test Selection with Test Purposes for Non-Deterministic Timed Automata
Nathalie Bertrand, Thierry Jéron, Amelie Stainer, and Moez Krichen
Applying CEGAR to the Petri Net State Equation
Karsten Wolf and Harro Wimmel
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
Alberto Griggio, Thi Thieu Hoa Le, and Roberto Sebastiani
Litmus: Running Tests Against Hardware
Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell
Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems
Tino Teige and Martin Fränzle
Efficient CTMC Model Checking of Linear Real-Time Objectives
Benoit Barbot, Taolue Chen, Tingting Han, Joost-Pieter Katoen, and Alexandru Mereacre
QUASY: Quantitative Synthesis Tool
Krishnendu Chatterjee, Thomas Henzinger, Barbara Jobstmann, and Rohit Singh
S-TALIRO: A Tool for Temporal Logic Falsification for Hybrid Systems
Yashwanth Annapureddy, Che Liu, Georgios Fainekos, and Sriram Sankaranarayanan
Compositionality entails sequentializability
Pranav Garg and P Madhusudan
Invariant Generation in Vampire
Kryštof Hoder, Laura Kovács, and Andrei Voronkov
Specification based Program Repair using SAT
Divya Gopinath, Zubair Malik, and Sarfraz Khurshid
Enforcing Structural Invariants using Dynamic Frames
Diego Garbervetsky, Daniel Gorín, and Ariel Neisen
Modelling and Verification of Web Services Business Activity Protocol
Saleem Vighio, Jiri Srba, and Anders P. Ravn
On Probabilistic Parallel Programs with Process Creation and Synchronisation
Stefan Kiefer and Dominik Wojtczak
Boosting Lazy Abstraction for SystemC with Partial Order Reduction
Alessandro Cimatti, Iman Narasamdya, and Marco Roveri
Unbeast: Symbolic Bounded Synthesis
Rüdiger Ehlers
CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe
Confluence reduction for probabilistic systems
Mark Timmer, Mariëlle Stoelinga, and Jaco van de Pol
Biased Model Checking using Flows
Muralidhar Talupur and Hyojung Han
The ACL2 Sedan Theorem Proving System
Harsh Raju Chamarthi, Peter C. Dillinger, Panagiotis Manolios, and Daron Vroon
Model Repair for Probabilistic Systems
Ezio Bartocci, Radu Grosu, Panagiotis Katsaros, CR Ramakrishnan, and Scott Smolka
Loop summarization and termination analysis
Aliaksei Tsitovich, Christoph M. Wintersteiger, Daniel Kroening, and Natasha Sharygina
GameTime: A Toolkit for Timing Analysis of Software
Sanjit A. Seshia and Jonathan Kotker
Quantitative Multi-Objective Verification for Probabilistic Systems
Vojtech Forejt, Marta Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu

Program Committee Co-Chairs

Tool Chair

Invited Speaker

Program Committee

TACAS Steering Committee