TACAS 2007

Thirteenth 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 2007) 24 March - 1 April, 2007, Braga, Portugal

Conference description | Call for papers | Important dates | Submission guidelines |  Programme Committee |  Invited Speaker |  Steering Committee

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 2007 is the tenth joint conference in this series. The conference is organized by the Universidade do Minho. 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, and ETAPS 2006 in Vienna.

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

ETAPS 2007 conferences and other satellite events will be held 24 March - 1 April, 2007.

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

23:59 EST on 6 October, 2006	Strict deadline for submission of abstracts (of research papers and tool demonstration papers)
23:59 EST on 13 October, 2006	Strict deadline for submission of full versions (of research papers and tool demonstration papers)
8 December, 2006	Acceptance notification of authors
23:59 EST on 5 January, 2007	Camera-ready paper versions due
26-30 March 2007	TACAS 2007 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.

We are pleased to announce awards sponsored by Microsoft Research Cambridge:

Up to seven (co)authors of papers to be accepted for TACAS'07 will be given an award if

• they have student status at any point of time between the submission and presentation of their paper
  
• their paper is among the seven best of those papers that are (co)authored by someone with student status as specified in the previous item **and** will be presented by a student.

No more than one award can be made to a single person or paper. All authors of accepted papers have been notified of these eligibility criteria. Nominations have to be sent to the co-chairs by Saturday, 23 December 2006.

The awardees are:

Jinqing Yu
Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams
Jinqing Yu, Gianfranco Ciardo, and Gerald Luettgen

Laurent Doyen
Improved algorithms for the automata based approach to model-checking
Laurent Doyen and Jean-Francois Raskin

Mariano M. Moscato
Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications
Marcelo F. Frias, Carlos G. Lopez Pombo, and Mariano M. Moscato

Zvonimir Rakamaric
A reachability predicate for analyzing low-level software
Shaunak Chatterjee, Shuvendu K. Lahiri, Shaz Qadeer, and Zvonimir Rakamaric

Pavol Cerny
Model Checking of Tree Logics with Path Equivalences
Rajeev Alur, Pavol Cerny, and Swarat Chaudhuri

Ru-Gang Xu
State of the Union: Type Inference via Craig Interpolation
Ranjit Jhala, Rupak Majumdar, and Ru-Gang Xu

Ahmed Rezine
Regular Model Checking without Transducers (On Efficient Verification of Parameterized Systems)
Parosh Aziz Abdulla, Giorgio Delzanno, Noomene Ben Henda, and Ahmed Rezine

Papers should be submitted using the TACAS 2007 Conference Service, which is now operative.

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

• 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 2007 Conference Service, which is now operative, (abstract no later than 23:59 EST on 6 October, 2006, and full paper no later than 23:59 EST on 13 October, 2006)

Tool demonstration papers

• 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:
  • how the oral presentation will be conducted, e.g. illustrated by a number of snapshots,
  • the availability of the tool, the number and types of users, other information which may illustrate the maturity and robustness of the tool,
  • 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 2007 Conference Service, which is now operative, (abstract no later than 23:59 EST on 6 October, 2006, and full paper no later than 23:59 on EST 13 October, 2006)

PROGRAMME COMMITTEE CO-CHAIRS

• Orna Grumberg, TECHNION - Israel Institute of Technology, Haifa (Israel)
• Michael Huth, Imperial College London, London (UK)

TOOL CHAIR

• Byron Cook, Microsoft Research, Cambridge (UK)

INVITED SPEAKER

• K. Rustan M. Leino, Microsoft Research, Redmond, Washington (USA)