From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 058447EE4A for ; Sat, 21 Sep 2013 05:40:42 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of klaus.havelund@jpl.nasa.gov) identity=pra; client-ip=128.149.139.105; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="klaus.havelund@jpl.nasa.gov"; x-sender="klaus.havelund@jpl.nasa.gov"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of klaus.havelund@jpl.nasa.gov) identity=mailfrom; client-ip=128.149.139.105; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="klaus.havelund@jpl.nasa.gov"; x-sender="klaus.havelund@jpl.nasa.gov"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail.jpl.nasa.gov) identity=helo; client-ip=128.149.139.105; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="klaus.havelund@jpl.nasa.gov"; x-sender="postmaster@mail.jpl.nasa.gov"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ai4BADoUPVKAlYtpnGdsb2JhbABRCgKDPYZcrTeJYIQ8I4EPDgEBAQEBCAsJCRQogh0sSz4bYh4SEIVdgg8MmXOhKI0QgRIEgR0eAhOCbiaBAAOJOI8OhVMUhhWGa4IJgUgCHgY X-IPAS-Result: Ai4BADoUPVKAlYtpnGdsb2JhbABRCgKDPYZcrTeJYIQ8I4EPDgEBAQEBCAsJCRQogh0sSz4bYh4SEIVdgg8MmXOhKI0QgRIEgR0eAhOCbiaBAAOJOI8OhVMUhhWGa4IJgUgCHgY X-IronPort-AV: E=Sophos;i="4.90,950,1371074400"; d="scan'208,217";a="33756888" Received: from mailhost.jpl.nasa.gov (HELO mail.jpl.nasa.gov) ([128.149.139.105]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 21 Sep 2013 05:40:39 +0200 Received: from [192.168.0.6] (cpe-76-170-88-117.socal.res.rr.com [76.170.88.117]) (authenticated (0 bits)) by smtp.jpl.nasa.gov (Sentrion-MTA-4.3.1/Sentrion-MTA-4.3.1) with ESMTP id r8L3d6Zb029817 (using TLSv1/SSLv3 with cipher AES128-SHA (128 bits) verified NO); Fri, 20 Sep 2013 20:39:08 -0700 From: Klaus Havelund Content-Type: multipart/alternative; boundary="Apple-Mail=_79AD2043-E1F6-44B8-9A7B-9BD86FF2C64A" Date: Fri, 20 Sep 2013 20:39:16 -0700 Message-Id: <7DA40966-63C2-439C-B997-813C353EC479@jpl.nasa.gov> Mime-Version: 1.0 (Mac OS X Mail 6.3 \(1503\)) X-Mailer: Apple Mail (2.1503) X-Source-Sender: klaus.havelund@jpl.nasa.gov X-JPL-Spam-Score': 80% X-Validation-by: klaus.havelund@jpl.nasa.gov Subject: [Caml-list] TACAS 2014 3rd call for papers --Apple-Mail=_79AD2043-E1F6-44B8-9A7B-9BD86FF2C64A Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=iso-8859-1 =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D THIRD CALL FOR PAPERS TACAS 2014 An ETAPS Member Conference 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems http://www.etaps.org/2014/tacas Abstract Submission: 4 October 2013 Paper Submission: 11 October 2013 Author Notification: 20 December 2013 =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D 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 with this common interest and to support them in their quest to improve the utility, reliability, flexibility and efficiency of tools and algorithms for building systems. Theoretical papers with clear relevance for tool construction and analysis, as well as tool descriptions and case studies with a conceptual message, are all encouraged. The topics covered by the conference include, but are not limited to: - Specification and verification techniques - Software and hardware verification - Analytical techniques for real-time, hybrid, or stochastic systems - Analytical techniques for safety, security, or dependability - Model checking - Theorem proving - SAT and SMT solvers - Static and dynamic program analysis - Testing - Abstraction techniques for modeling and verification - Compositional and refinement-based methodologies - System construction and transformation techniques - Tool environments and tool architectures - Applications and case studies =3D=3D=3D Paper categories: =3D=3D=3D TACAS accepts four types of submissions: research papers, case study papers, regular tool papers, and tool demonstration papers. - Research papers clearly identify and justify a principled advance to the theoretical foundations for the construction and analysis of systems and, where applicable, are supported by experimental validation. Research papers can have a maximum of 15 pages. - Case study papers report on case studies (preferably in a "real life" setting). They should provide information about the following aspects: the system being studied and why it is of interest, the goals of the study, the challenges the system poses to automated analysis, research methodologies and the approach used, the degree to which goals were attained, and how the results can be generalized to other problems and domains. Case study papers can have a maximum of 15 pages. - Regular tool papers present a new tool, a new tool component, or novel extensions to an existing tool. They should provide a short description of the theoretical foundations with relevant citations, and emphasize the design and implementation concerns including software architecture and core data structures. A regular tool paper should give a clear account of the tool's functionality, discuss the tool's practical capabilities with reference to the type and size of problems it can handle, experience with realistic case studies, and where applicable, provide a rigorous experimental evaluation. Papers that present extensions to existing tools should clearly focus on the improvements or extensions with respect to previously published versions of the tool, preferably substantiated by data on enhancements in terms of resources and capabilities. We strongly suggest authors make their tools available via the web, even if only for the evaluation process. Tool papers can have a maximum of 15 pages. - Tool demonstration papers focus on the usage aspects of tools. The described tools must be publicly available. Theoretical foundations and experimental evaluation are not required, however, a motivation as to why the tool is interesting and significant should be provided. Tool demonstration papers can have a maximum of 6 pages. They should have an appendix of up to 6 additional pages with details on the actual demonstration. The proceedings will be published in the Advanced Research in Computing and Software Science (ARCoSS) subline of Springer's Lecture Notes in Computer Science series. Papers of all four types will appear in the proceedings and have presentations during the conference. =3D=3D=3D Submission: =3D=3D=3D A condition of submission is that, if the submission is accepted, one of the authors attends the conference to give the presentation. Submitted papers must be in English presenting unpublished research not submitted for publication elsewhere. In particular, simultaneous submission of the same contribution to multiple ETAPS conferences is forbidden. Papers must follow the formatting guidelines specified by Springer at the URL: http://www.springer.de/comp/lncs/authors.html and be submitted electronically in pdf through Easychair: https://www.easychair.org/account/signin.cgi?conf=3Dtacas2014. Submissions not adhering to the specified format and length may be rejected immediately. =3D=3D=3D Competition on Software Verification: =3D=3D=3D TACAS 2014 hosts the third competition on software verification with the goal to evaluate technology transfer and compare state-of-the-art software verifiers with respect to effectiveness and efficiency. More information can be found on the competition website: http://sv-comp.sosy-lab.org/2014. =3D=3D=3D Invited Speaker: =3D=3D=3D Orna Kupferman (Hebrew University Jerusalem, Israel) =3D=3D=3D Programme Chairs: =3D=3D=3D Erika =C1brah=E1m (RWTH Aachen University, Germany) Klaus Havelund (NASA JPL, USA) =3D=3D=3D Tool Chair: =3D=3D=3D Nikolaj Bj=F8rner (Microsoft Research, USA) =3D=3D=3D Programme Committee: =3D=3D=3D Christel Baier (Technical University of Dresden, Germany) Saddek Bensalem (VERIMAG/UJF, France) Nathalie Bertrand (IRISA Rennes, France) Armin Biere (Johannes Kepler University, Austria) Nikolaj Bj=F8rner (Microsoft Research, USA) Rance Cleaveland (University of Maryland, USA) Alessandro Cimatti (Fondazione Bruno Kessler, Italy) Cindy Eisner (IBM Research Haifa, Israel) Martin Fr=E4nzle (Carl von Ossietzky University Oldenburg, Germany) Patrice Godefroid (Microsoft Research, Redmond, USA) Susanne Graf (Verimag, France) Orna Grumberg (Technion, Israel) Boudewijn Haverkort (University of Twente, the Netherlands) Gerard Holzmann (NASA JPL, USA) Barbara Jobstmann (CNRS, Verimag, France) Joost-Pieter Katoen (RWTH Aachen University, Germany, and University of Twente, the Netherlands) Kim Larsen (Aalborg University, Denmark) Roland Meyer (TU Kaiserslautern, Germany) Corina Pasareanu (NASA Ames Research Center, USA) Doron Peled (Bar Ilan University, Israel) Paul Pettersson (M=E4lardalen University, Sweden) Nir Piterman (University of Leicester, UK) Jaco van de Pol (University of Twente, the Netherlands) Sriram Sankaranarayanan (University of Colorado Boulder, USA) Natasha Sharygina (Universita della Svizzera Italiana, Switzerland) Scott Smolka (Stony Brook University, USA) Bernhard Steffen (University of Dortmund, Germany) Marielle Stoelinga (University of Twente, the Netherlands) Cesare Tinelli (University of Iowa, USA) Fritz Vaandrager (Radboud University Nijmegen, The Netherlands) Willem Visser (University of Stellenbosch, South Africa) Ralf Wimmer (University of Freiburg, Germany) Lenore Zuck (University of Illinois at Chicago, USA) =3D=3D=3D Steering Committee: =3D=3D=3D Rance Cleaveland (University of Maryland, USA) Holger Hermanns (Saarland University, Germany) Kim G. Larsen (Aalborg University, Denmark) Bernhard Steffen (TU Munich, Germany) Lenore Zuck (University of Illinois at Chicago, USA)= --Apple-Mail=_79AD2043-E1F6-44B8-9A7B-9BD86FF2C64A Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=iso-8859-1

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
          &nb= sp;      THIRD CALL FOR PAPERS

   &nbs= p;            &= nbsp;     TACAS 2014
    &n= bsp;         An ETAPS Member C= onference

20th International Conference on Tools and Algorithms for = the
Construction and Analysis of Systems

    =         http://www.etaps.org/2014/tacas

Abstract Submis= sion: 4 October 2013
Paper Submission: 11 October 2013
Author Notific= ation: 20 December 2013
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

TACAS i= s 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= with this common interest and to support them
in their quest to improve= the utility, reliability, flexibility and
efficiency of tools and algor= ithms for building systems.

Theoretical papers with clear relevance = for tool construction and
analysis, as well as tool descriptions and cas= e studies with a
conceptual message, are all encouraged. The topics cove= red by the
conference include, but are not limited to:

- Specific= ation and verification techniques
- Software and hardware verification- Analytical techniques for real-time, hybrid, or stochastic systems
-= Analytical techniques for safety, security, or dependability
- Model ch= ecking
- Theorem proving
- SAT and SMT solvers
- Static and dynami= c program analysis
- Testing
- Abstraction techniques for modeling an= d verification
- Compositional and refinement-based methodologies
- S= ystem construction and transformation techniques
- Tool environments and= tool architectures
- Applications and case studies

=3D=3D=3D Pap= er categories: =3D=3D=3D

TACAS accepts four types of submissions: re= search papers, case study
papers, regular tool papers, and tool demonstr= ation papers.

- Research papers clearly identify and justify a princ= ipled advance
to the theoretical foundations for the construction and an= alysis of
systems and, where applicable, are supported by experimentalvalidation. Research papers can have a maximum of 15 pages.

- Case= study papers report on case studies (preferably in a "real
life" settin= g). They should provide information about the following
aspects: the sys= tem being studied and why it is of interest, the
goals of the study, the= challenges the system poses to automated
analysis, research methodologi= es and the approach used, the degree to
which goals were attained, and h= ow the results can be generalized to
other problems and domains. Case st= udy papers can have a maximum of
15 pages.

- Regular tool papers = present a new tool, a new tool component, or
novel extensions to an exis= ting tool. They should provide a short
description of the theoretical fo= undations with relevant citations,
and emphasize the design and implemen= tation concerns including
software architecture and core data structures= . A regular tool paper
should give a clear account of the tool's functio= nality, discuss the
tool's practical capabilities with reference to the = type and size of
problems it can handle, experience with realistic case = studies, and
where applicable, provide a rigorous experimental evaluatio= n. Papers
that present extensions to existing tools should clearly focus= on the
improvements or extensions with respect to previously published<= br>versions of the tool, preferably substantiated by data on
enhancement= s in terms of resources and capabilities. We strongly
suggest authors ma= ke their tools available via the web, even if only
for the evaluation pr= ocess. Tool papers can have a maximum of 15
pages.

- Tool demonst= ration papers focus on the usage aspects of tools. The
described tools m= ust be publicly available. Theoretical foundations
and experimental eval= uation are not required, however, a motivation
as to why the tool is int= eresting and significant should be provided.
Tool demonstration papers c= an have a maximum of 6 pages. They should
have an appendix of up to 6 ad= ditional pages with details on the
actual demonstration.

The proc= eedings will be published in the Advanced Research in
Computing and Soft= ware Science (ARCoSS) subline of Springer's Lecture
Notes in Computer Sc= ience series. Papers of all four types will
appear in the proceedings an= d have presentations during the
conference.

=3D=3D=3D Submission:= =3D=3D=3D

A condition of submission is that, if the submission is a= ccepted, one
of the authors attends the conference to give the presentat= ion.
Submitted papers must be in English presenting unpublished research=
not submitted for publication elsewhere. In particular, simultaneoussubmission of the same contribution to multiple ETAPS conferences is
fo= rbidden. Papers must follow the formatting guidelines specified by
Sprin= ger at the URL: http://www.springer.de/comp/lncs/authors.html
and be submitted e= lectronically in pdf through Easychair:
https://www.easychair.org/account= /signin.cgi?conf=3Dtacas2014.
Submissions not adhering to the specif= ied format and length may be
rejected immediately.

=3D=3D=3D Comp= etition on Software Verification: =3D=3D=3D

TACAS 2014 hosts the thi= rd competition on software verification with
the goal to evaluate techno= logy transfer and compare state-of-the-art
software verifiers with respe= ct to effectiveness and efficiency. More
information can be found on the= competition website:
http:= //sv-comp.sosy-lab.org/2014.

=3D=3D=3D Invited Speaker: =3D=3D= =3D

  Orna Kupferman (Hebrew University Jerusalem, Israel)=

=3D=3D=3D Programme Chairs: =3D=3D=3D

  Erika =C1b= rah=E1m (RWTH Aachen University, Germany)
  Klaus Havelund (NA= SA JPL, USA)

=3D=3D=3D Tool Chair: =3D=3D=3D

  Niko= laj Bj=F8rner (Microsoft Research, USA)

=3D=3D=3D Programme Committe= e: =3D=3D=3D

  Christel Baier (Technical University of Dre= sden, Germany)
  Saddek Bensalem (VERIMAG/UJF, France)
&nbs= p; Nathalie Bertrand (IRISA Rennes, France)
  Armin Biere= (Johannes Kepler University, Austria)
  Nikolaj Bj=F8rner (Mi= crosoft Research, USA)
  Rance Cleaveland (University of Maryl= and, USA)
  Alessandro Cimatti (Fondazione Bruno Kessler, Ital= y)
  Cindy Eisner (IBM Research Haifa, Israel)
  = Martin Fr=E4nzle (Carl von Ossietzky University Oldenburg, Germany)
&nbs= p; Patrice Godefroid (Microsoft Research, Redmond, USA)
  = ;Susanne Graf (Verimag, France)
  Orna Grumberg (Technion, Isr= ael)
  Boudewijn Haverkort (University of Twente, the Netherla= nds)
  Gerard Holzmann (NASA JPL, USA)
  Barbara = Jobstmann (CNRS, Verimag, France)
  Joost-Pieter Katoen (RWTH = Aachen University, Germany, and
     University= of Twente, the Netherlands)
  Kim Larsen (Aalborg University,= Denmark)
  Roland Meyer (TU Kaiserslautern, Germany)
 = ; Corina Pasareanu (NASA Ames Research Center, USA)
  Dor= on Peled (Bar Ilan University, Israel)
  Paul Pettersson (M=E4= lardalen University, Sweden)
  Nir Piterman (University of Lei= cester, UK)
  Jaco van de Pol (University of Twente, th= e Netherlands)
  Sriram Sankaranarayanan (University of Colora= do Boulder, USA)
  Natasha Sharygina (Universita della Svizzer= a Italiana, Switzerland)
  Scott Smolka (Stony Brook Universit= y, USA)
  Bernhard Steffen (University of Dortmund, Germany)  Marielle Stoelinga (University of Twente, the Netherlands)
  Cesare Tinelli (University of Iowa, USA)
  Frit= z Vaandrager (Radboud University Nijmegen, The Netherlands)
  = Willem Visser (University of Stellenbosch, South Africa)
  Ral= f Wimmer (University of Freiburg, Germany)
  Lenore Zuck (Univ= ersity of Illinois at Chicago, USA)

=3D=3D=3D Steering Co= mmittee: =3D=3D=3D

  Rance Cleaveland (University of Maryl= and, USA)
  Holger Hermanns (Saarland University, Germany)
=   Kim G. Larsen (Aalborg University, Denmark)
  Bern= hard Steffen (TU Munich, Germany)
  Lenore Zuck (University of= Illinois at Chicago, USA)
= --Apple-Mail=_79AD2043-E1F6-44B8-9A7B-9BD86FF2C64A--