<html><head><meta http-equiv="Content-Type" content="text/html charset=iso-8859-1"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><br></div><div><div>============================================================<br>&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;THIRD CALL FOR PAPERS<br><br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;TACAS 2014<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;An ETAPS Member Conference<br><br>20th International Conference on Tools and Algorithms for the<br>Construction and Analysis of Systems<br><br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a href="http://www.etaps.org/2014/tacas">http://www.etaps.org/2014/tacas</a><br><br>Abstract Submission: 4 October 2013<br>Paper Submission: 11 October 2013<br>Author Notification: 20 December 2013<br>=============================================================<br><br>TACAS is a forum for researchers, developers and users interested in<br>rigorously based tools and algorithms for the construction and<br>analysis of systems. The conference serves to bridge the gaps between<br>different communities with this common interest and to support them<br>in their quest to improve the utility, reliability, flexibility and<br>efficiency of tools and algorithms for building systems.<br><br>Theoretical papers with clear relevance for tool construction and<br>analysis, as well as tool descriptions and case studies with a<br>conceptual message, are all encouraged. The topics covered by the<br>conference include, but are not limited to:<br><br>- Specification and verification techniques<br>- Software and hardware verification<br>- Analytical techniques for real-time, hybrid, or stochastic systems<br>- Analytical techniques for safety, security, or dependability<br>- Model checking<br>- Theorem proving<br>- SAT and SMT solvers<br>- Static and dynamic program analysis<br>- Testing<br>- Abstraction techniques for modeling and verification<br>- Compositional and refinement-based methodologies<br>- System construction and transformation techniques<br>- Tool environments and tool architectures<br>- Applications and case studies<br><br>=== Paper categories: ===<br><br>TACAS accepts four types of submissions: research papers, case study<br>papers, regular tool papers, and tool demonstration papers.<br><br>- Research papers clearly identify and justify a principled advance<br>to the theoretical foundations for the construction and analysis of<br>systems and, where applicable, are supported by experimental<br>validation. Research papers can have a maximum of 15 pages.<br><br>- Case study papers report on case studies (preferably in a "real<br>life" setting). They should provide information about the following<br>aspects: the system being studied and why it is of interest, the<br>goals of the study, the challenges the system poses to automated<br>analysis, research methodologies and the approach used, the degree to<br>which goals were attained, and how the results can be generalized to<br>other problems and domains. Case study papers can have a maximum of<br>15 pages.<br><br>- Regular tool papers present a new tool, a new tool component, or<br>novel extensions to an existing tool. They should provide a short<br>description of the theoretical foundations with relevant citations,<br>and emphasize the design and implementation concerns including<br>software architecture and core data structures. A regular tool paper<br>should give a clear account of the tool's functionality, discuss the<br>tool's practical capabilities with reference to the type and size of<br>problems it can handle, experience with realistic case studies, and<br>where applicable, provide a rigorous experimental evaluation. Papers<br>that present extensions to existing tools should clearly focus on the<br>improvements or extensions with respect to previously published<br>versions of the tool, preferably substantiated by data on<br>enhancements in terms of resources and capabilities. We strongly<br>suggest authors make their tools available via the web, even if only<br>for the evaluation process. Tool papers can have a maximum of 15<br>pages.<br><br>- Tool demonstration papers focus on the usage aspects of tools. The<br>described tools must be publicly available. Theoretical foundations<br>and experimental evaluation are not required, however, a motivation<br>as to why the tool is interesting and significant should be provided.<br>Tool demonstration papers can have a maximum of 6 pages. They should<br>have an appendix of up to 6 additional pages with details on the<br>actual demonstration.<br><br>The proceedings will be published in the Advanced Research in<br>Computing and Software Science (ARCoSS) subline of Springer's Lecture<br>Notes in Computer Science series. Papers of all four types will<br>appear in the proceedings and have presentations during the<br>conference.<br><br>=== Submission: ===<br><br>A condition of submission is that, if the submission is accepted, one<br>of the authors attends the conference to give the presentation.<br>Submitted papers must be in English presenting unpublished research<br>not submitted for publication elsewhere. In particular, simultaneous<br>submission of the same contribution to multiple ETAPS conferences is<br>forbidden. Papers must follow the formatting guidelines specified by<br>Springer at the URL:&nbsp;<a href="http://www.springer.de/comp/lncs/authors.html">http://www.springer.de/comp/lncs/authors.html</a><br>and be submitted electronically in pdf through Easychair:<br><a href="https://www.easychair.org/account/signin.cgi?conf=tacas2014">https://www.easychair.org/account/signin.cgi?conf=tacas2014</a>.<br>Submissions not adhering to the specified format and length may be<br>rejected immediately.<br><br>=== Competition on Software Verification: ===<br><br>TACAS 2014 hosts the third competition on software verification with<br>the goal to evaluate technology transfer and compare state-of-the-art<br>software verifiers with respect to effectiveness and efficiency. More<br>information can be found on the competition website:<br><a href="http://sv-comp.sosy-lab.org/2014">http://sv-comp.sosy-lab.org/2014</a>.<br><br>=== Invited Speaker: ===<br><br>&nbsp;&nbsp;Orna Kupferman (Hebrew University Jerusalem, Israel)<br><br>=== Programme Chairs: ===<br><br>&nbsp;&nbsp;Erika Ábrahám (RWTH Aachen University, Germany)<br>&nbsp;&nbsp;Klaus Havelund (NASA JPL, USA)<br><br>=== Tool Chair: ===<br><br>&nbsp;&nbsp;Nikolaj Bjørner (Microsoft Research, USA)<br><br>=== Programme Committee: ===<br><br>&nbsp;&nbsp;Christel Baier (Technical University of Dresden, Germany)<br>&nbsp;&nbsp;Saddek Bensalem (VERIMAG/UJF, France)<br>&nbsp;&nbsp;Nathalie Bertrand (IRISA Rennes, France)<br>&nbsp;&nbsp;Armin Biere (Johannes Kepler University, Austria)<br>&nbsp;&nbsp;Nikolaj Bjørner (Microsoft Research, USA)<br>&nbsp;&nbsp;Rance Cleaveland (University of Maryland, USA)<br>&nbsp;&nbsp;Alessandro Cimatti (Fondazione Bruno Kessler, Italy)<br>&nbsp;&nbsp;Cindy Eisner (IBM Research Haifa, Israel)<br>&nbsp;&nbsp;Martin Fränzle (Carl von Ossietzky University Oldenburg, Germany)<br>&nbsp;&nbsp;Patrice Godefroid (Microsoft Research, Redmond, USA)<br>&nbsp;&nbsp;Susanne Graf (Verimag, France)<br>&nbsp;&nbsp;Orna Grumberg (Technion, Israel)<br>&nbsp;&nbsp;Boudewijn Haverkort (University of Twente, the Netherlands)<br>&nbsp;&nbsp;Gerard Holzmann (NASA JPL, USA)<br>&nbsp;&nbsp;Barbara Jobstmann (CNRS, Verimag, France)<br>&nbsp;&nbsp;Joost-Pieter Katoen (RWTH Aachen University, Germany, and<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;University of Twente, the Netherlands)<br>&nbsp;&nbsp;Kim Larsen (Aalborg University, Denmark)<br>&nbsp;&nbsp;Roland Meyer (TU Kaiserslautern, Germany)<br>&nbsp;&nbsp;Corina Pasareanu (NASA Ames Research Center, USA)<br>&nbsp;&nbsp;Doron Peled (Bar Ilan University, Israel)<br>&nbsp;&nbsp;Paul Pettersson (Mälardalen University, Sweden)<br>&nbsp;&nbsp;Nir Piterman (University of Leicester, UK)</div><div>&nbsp; Jaco van de Pol&nbsp;(University of Twente, the Netherlands)<br>&nbsp;&nbsp;Sriram Sankaranarayanan (University of Colorado Boulder, USA)<br>&nbsp;&nbsp;Natasha Sharygina (Universita della Svizzera Italiana, Switzerland)<br>&nbsp;&nbsp;Scott Smolka (Stony Brook University, USA)<br>&nbsp;&nbsp;Bernhard Steffen (University of Dortmund, Germany)<br>&nbsp;&nbsp;Marielle Stoelinga (University of Twente, the Netherlands)</div><div>&nbsp; Cesare Tinelli (University of Iowa, USA)<br>&nbsp;&nbsp;Fritz Vaandrager (Radboud University Nijmegen, The Netherlands)<br>&nbsp;&nbsp;Willem Visser (University of Stellenbosch, South Africa)<br>&nbsp;&nbsp;Ralf Wimmer (University of Freiburg, Germany)<br>&nbsp;&nbsp;Lenore Zuck (University of Illinois at Chicago, USA)<br><br></div><div>=== Steering Committee: ===<br><br>&nbsp;&nbsp;Rance Cleaveland (University of Maryland, USA)<br>&nbsp;&nbsp;Holger Hermanns (Saarland University, Germany)<br>&nbsp;&nbsp;Kim G. Larsen (Aalborg University, Denmark)<br>&nbsp;&nbsp;Bernhard Steffen (TU Munich, Germany)<br>&nbsp;&nbsp;Lenore Zuck (University of Illinois at Chicago, USA)</div></div><div><br></div><div><br></div></body></html>