From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr 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 4D5AA7FD90 for ; Mon, 12 Dec 2016 15:03:53 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fm-announcements-bounces@lists.nasa.gov; spf=Pass smtp.mailfrom=fm-announcements-bounces@lists.nasa.gov; spf=Pass smtp.helo=postmaster@lists.nasa.gov Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of fm-announcements-bounces@lists.nasa.gov) identity=pra; client-ip=128.156.249.229; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="fm-announcements-bounces@lists.nasa.gov"; x-sender="fm-announcements-bounces@lists.nasa.gov"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of fm-announcements-bounces@lists.nasa.gov designates 128.156.249.229 as permitted sender) identity=mailfrom; client-ip=128.156.249.229; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="fm-announcements-bounces@lists.nasa.gov"; x-sender="fm-announcements-bounces@lists.nasa.gov"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of postmaster@lists.nasa.gov designates 128.156.249.229 as permitted sender) identity=helo; client-ip=128.156.249.229; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="fm-announcements-bounces@lists.nasa.gov"; x-sender="postmaster@lists.nasa.gov"; x-conformance=sidf_compatible; x-record-type="v=spf1" IronPort-PHdr: =?us-ascii?q?9a23=3AthiPqRXHHaS/SFTP2L+3nH21dYDV8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYZxOCt8tkgFKBZ4jH8fUM07OQ6PG7HzJaqs/Q+DBaKdoXCE9D0Z?= =?us-ascii?q?1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5y?= =?us-ascii?q?O/inUtWK15f/hKiP/YbOaVBNjTu5fbQgIhDzpAPXsdQQioZnJ6At0V7Tr2JVdv?= =?us-ascii?q?9K7WdpPk6I2RD1/c7285l9pD9NsfAs/NIVTKPhYq4jRqZZBjl1DmYu+ce+tQXf?= =?us-ascii?q?VRDdoTwYU34KiVxOChPMqh79QND0uyr+s+N7ny6CIczxS6tzVzHn5qFtTwLugy?= =?us-ascii?q?oCOjgl6zLrjZk6gqceqRSnoAF5yIPRbYeJL9J6f7jBZpUcTHFIGMlWSWYJVo25?= =?us-ascii?q?KoIJCe0cO+1VqoT7u0AmqRqlGRLqAur0w3lHgWGgjoMg1OF0WyHPwgEkAtQC9D?= =?us-ascii?q?z3qNzoL+9SCrzl5uiChWHga/pLwnHd4ZbFdg0nrdmORbY2d8PKwA8gEB2T3QbY?= =?us-ascii?q?kpDsIz7AjrdFiGOc9ec1De8=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BWAAB9rU5YmOX5nIBdGwEBAQMBAQEJA?= =?us-ascii?q?QEBFgEBAQMBAQEJAQEBgkg5CwEBAQEBaw5WBykHAY1BrBeCBQUcAQqCQoNYgU4?= =?us-ascii?q?/FAEBAQEBAQEBAQEBEgEBAQEBCAsLBx0lC4IzBAIDDweCHQEBARUFKQgCGAYOA?= =?us-ascii?q?wECBgIBAUABAQQIAwEkCQEnBAoJBREGAQSISgUJqikCg1CLFwELJjKGDYYXAYF?= =?us-ascii?q?NgQ8KBwGFfQWPP4srAQGGToVwhyuHRYY9khgREIEZHkODBEgngUVyhV4CDRcHK?= =?us-ascii?q?VoBgQwBAQE?= X-IPAS-Result: =?us-ascii?q?A0BWAAB9rU5YmOX5nIBdGwEBAQMBAQEJAQEBFgEBAQMBAQE?= =?us-ascii?q?JAQEBgkg5CwEBAQEBaw5WBykHAY1BrBeCBQUcAQqCQoNYgU4/FAEBAQEBAQEBA?= =?us-ascii?q?QEBEgEBAQEBCAsLBx0lC4IzBAIDDweCHQEBARUFKQgCGAYOAwECBgIBAUABAQQ?= =?us-ascii?q?IAwEkCQEnBAoJBREGAQSISgUJqikCg1CLFwELJjKGDYYXAYFNgQ8KBwGFfQWPP?= =?us-ascii?q?4srAQGGToVwhyuHRYY9khgREIEZHkODBEgngUVyhV4CDRcHKVoBgQwBAQE?= X-IronPort-AV: E=Sophos;i="5.33,336,1477954800"; d="scan'208,217";a="249532558" Received: from lists.nasa.gov ([128.156.249.229]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 12 Dec 2016 15:03:51 +0100 Received: from localhost (localhost [127.0.0.1]) by lists.nasa.gov (Postfix) with ESMTP id 4DA9260285A; Mon, 12 Dec 2016 09:02:17 -0500 (EST) Received: from lists.nasa.gov ([127.0.0.1]) by localhost (lists.nasa.gov [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id eL0oVxJZ2sWD; Mon, 12 Dec 2016 09:02:17 -0500 (EST) Received: from LISTS.nasa.gov (localhost [127.0.0.1]) by lists.nasa.gov (Postfix) with ESMTP id 33E57601D58; Mon, 12 Dec 2016 09:02:13 -0500 (EST) X-Original-To: fm-announcements@lists.nasa.gov Delivered-To: fm-announcements@lists.nasa.gov Received: from localhost (localhost [127.0.0.1]) by lists.nasa.gov (Postfix) with ESMTP id F419A6017E8 for ; Mon, 12 Dec 2016 09:02:10 -0500 (EST) Received: from lists.nasa.gov ([127.0.0.1]) by localhost (lists.nasa.gov [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id K+3qGOmM+XZX for ; Mon, 12 Dec 2016 09:02:10 -0500 (EST) Received: from mail.jpl.nasa.gov (sentrion1.jpl.nasa.gov [128.149.139.105]) by lists.nasa.gov (Postfix) with ESMTPS id 438FB60138F for ; Mon, 12 Dec 2016 09:02:08 -0500 (EST) Received: from mail.jpl.nasa.gov (ap-ehub-sp02.jpl.nasa.gov [128.149.137.149]) by smtp.jpl.nasa.gov (Sentrion-MTA-4.3.1/Sentrion-MTA-4.3.1) with ESMTP id uBCE27fa008864 (using TLSv1 with cipher ECDHE-RSA-AES256-SHA (256 bits) verified NO) for ; Mon, 12 Dec 2016 06:02:07 -0800 Received: from AP-EMBX-SP20.RES.AD.JPL ([169.254.8.80]) by ap-ehub-sp02.RES.AD.JPL ([fe80::dd85:7b07:1e36:7e3c%15]) with mapi id 14.03.0279.002; Mon, 12 Dec 2016 06:02:07 -0800 From: "Havelund, Klaus (348B)" To: "fm-announcements@lists.nasa.gov" Thread-Topic: SPIN 2017 - 2nd Call for Papers *Paper Submission: February 10, 2017* Thread-Index: AQHSVIBSp75DBPVxykmStivp0zma0g== Date: Mon, 12 Dec 2016 14:02:06 +0000 Message-ID: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/14.7.0.161029 x-originating-ip: [128.149.137.82] MIME-Version: 1.0 X-Source-Sender: Klaus.Havelund@jpl.nasa.gov X-AUTH: Authorized X-BeenThere: fm-announcements@lists.nasa.gov X-Mailman-Version: 2.1.14 List-Id: NASA Formal Methods Announcements List-Unsubscribe: , List-Post: List-Help: List-Subscribe: , Content-Type: multipart/mixed; boundary="===============5389873631686806501==" Errors-To: fm-announcements-bounces@lists.nasa.gov Sender: fm-announcements-bounces@lists.nasa.gov X-Validation-by: klaus.havelund@jpl.nasa.gov Subject: [Caml-list] [fm-announcements] SPIN 2017 - 2nd Call for Papers *Paper Submission: February 10, 2017* --===============5389873631686806501== Content-Language: en-US Content-Type: multipart/alternative; boundary="_000_D473EDDF16B59klaushavelundjplnasagov_" --_000_D473EDDF16B59klaushavelundjplnasagov_ Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable SPIN 2017 24th International Symposium on Model Checking of Software Santa Barbara, CA, USA, July 13-14, 2017 http://conf.researchr.org/home/spin-2017 Collocated with ISSTA ________________________________ The SPIN symposium aims at bringing together researchers and practitioners = interested in automated tool-based techniques for the analysis of software = as well as models of software, for the purpose of verification and validati= on. The symposium specifically focuses on concurrent software, but does not= exclude analysis of sequential software. Submissions are solicited on theo= retical results, novel algorithms, tool development, empirical evaluation, = and education. History: The SPIN symposium originated as a workshop focusing on explicit s= tate model checking, specifically as related to the Spin model checker. How= ever, over the years it has evolved to a broadly scoped symposium for softw= are analysis using any automated techniques, including model checking, auto= mated theorem proving, and symbolic execution. SPIN 2017 will be organized as an ACM SIGSOFT event, collocated with the In= ternational Symposium on Software Testing and Analysis (ISSTA 2017): http:/= /conf.researchr.org/home/issta-2017. In addition there will be a one-day Ri= gorous Examination of Reactive Systems verification challenge Workshop (RER= S 2017): http://www.rers-challenge.org/2017. An overview of the previous SP= IN symposia (and early workshops) can be found at: http://spinroot.com/spin= /symposia. Topics of interest include, but are not limited to: * Formal verification techniques for automated analysis of software * Formal analysis for modeling languages, such as UML/state charts * Formal specification languages, temporal logic, design-by-contract * Model checking * Automated theorem proving, including SAT and SMT * Verifying compilers * Abstraction and symbolic execution techniques * Static analysis and abstract interpretation * Combination of verification techniques * Modular and compositional verification techniques * Verification of timed and probabilistic systems * Automated testing using advanced analysis techniques * Combination of static and dynamic analyses * Derivation of specifications, test cases, or other useful material vi= a formal analysis * Case studies of interesting systems or with interesting results * Engineering and implementation of software verification and analysis = tools * Benchmark and comparative studies for formal verification and analysi= s tools * Formal methods education and training * Insightful surveys or historical accounts on topics of relevance to t= he symposium ________________________________ Submission Guidelines ________________________________ The contributions to SPIN 2017 will be published as ACM Proceedings, and sh= ould be submitted in the ACM Conference Format: https://www.acm.org/publica= tions/proceedings-template. With the exception of survey and history papers, submissions must be origin= al and should not have been published previously or be under consideration = for publication while being evaluated for this symposium. We are soliciting two categories of papers: * Full Research Papers describing fully developed work and complete res= ults (10 pages); * Short Papers presenting tools, technology, experiences with lessons l= earned, new ideas, work in progress with preliminary results, and novel con= tributions to formal methods education (4 pages). Papers should be submitted via the EasyChair SPIN 2017 submission website: = https://easychair.org/conferences/?conf=3Dspin2017. Best Paper awards will be given and announced at the conference. A selection of papers will be invited to a special issue of the Internation= al Journal on Software Tools for Technology Transfer (STTT). ________________________________ Important Dates ________________________________ * Paper Submission: February 10, 2017 (23:59:59 Anywhere on Earth) * Author Notification : April 15, 2017 * Camera-Ready Paper: May 20, 2017 * Symposium : July 13-14, 2017 ________________________________ Organization ________________________________ * Hakan Erdogmus, Program Co-Chair, Carnegie Mellon University, USA * Klaus Havelund, Program Co-Chair, NASA/Caltech Jet Propulsion Laborat= ory, USA * Corina Pasareanu, Awards Chair, NASA Ames Research Center, USA * Yli=E8s Falcone, Publicity Chair, Univ. Grenoble Alpes, Inria, France ________________________________ Program Committee ________________________________ * Erika Abraham, RWTH Aachen University, Germany * Christel Baier, Technical University of Dresden, Germany * Tom Ball, Microsoft Research, USA * Ezio Bartocci, Vienna University of Technology, Austria * Dirk Beyer, Ludwig-Maximilians-Universit=E4t M=FCnchen (LMU Munich), = Germany * Armin Biere, Johannes Kepler University, Austria * Dragan Bosnacki, Eindhoven University of Technology, Netherlands * Zmago Brezocnik, University of Maribor, Slovenia * Sagar Chaki, Software Engineering Institute CMU, USA * Alessandro Cimatti, Fondazione Bruno Kessler, Italy * Lucas Cordeiro, University of Oxford, UK * Patrice Godefroid, Microsoft Research, USA * Susanne Graf, VERIMAG Laboratory, France * Radu Grosu, Vienna University of Technology, Austria * Arie Gurfinkel, University of Waterloo, USA * Gerard Holzmann, NASA/Caltech Jet Propulsion Laboratory, USA * Sarfraz Khurshid, The University of Texas at Austin, USA * Kim Larsen, Aalborg University, Denmark * Stefan Leue, University of Konstanz, Germany * Alice Miller, University of Glasgow, Scotland * Corina Pasareanu, NASA Ames Research Center, USA * Doron Peled, Bar Ilan University, Israel * Neha Rungta, NASA Ames Research Center, USA * Theo Ruys, RUwise, Netherlands * Scott Smolka, Stony Brook University, USA * Scott Stoller, Stony Brook University, United States * Jun Sun, Singapore University of Technology and Design, Singapore * Oksana Tkachuk, NASA Ames Research Center, USA * Stavros Tripakis, University of California, Berkeley, USA * Willem Visser, Stellenbosch University, South Africa * Farn Wang, National Taiwan University, Taiwan * Michael Whalen, University of Minnesota, USA * Anton Wijs, Eindhoven University of Technology, Netherlands ________________________________ Steering Committee ________________________________ * Dragan Bosnacki, Eindhoven University of Technology, Netherlands * Susanne Graf, Verimag, France * Gerard Holzmann, NASA/Caltech Jet Propulsion Laboratory, United States * Stefan Leue, University of Konstanz, Germany * Willem Visser, Stellenbosch University, South Africa --_000_D473EDDF16B59klaushavelundjplnasagov_ Content-Type: text/html; charset="iso-8859-1" Content-ID: <122F13AE0D38004A8B5F97C8315EB43B@ad.jpl> Content-Transfer-Encoding: quoted-printable

SPIN 2017


24th International Symposium on Model Checking of Software

Santa Barbara, C= A, USA, = July 13-14, 2017


http://conf.researchr.org/home= /spin-2017

Collocated with = ISSTA 

The SPIN symposium aims at bringing together researchers and practitioners = interested in automated tool-based techniques for the analysis of software = as well as models of software, for the purpose of verification and validati= on. The symposium specifically focuses on concurrent software, but does not exclude analysis of sequential softwa= re. Submissions are solicited on theoretical results, novel algorithms, too= l development, empirical evaluation, and education.

History: The SPIN symposium originated as a workshop focusing on explicit s= tate model checking, specifically as related to the Spin model checker. How= ever, over the years it has evolved to a broadly scoped symposium for softw= are analysis using any automated techniques, including model checking, automated theorem proving, and symbo= lic execution.

SPIN 2017 will be organized as an ACM SIGSOFT event, collocated with the In= ternational Symposium on Software Testing and Analysis (ISSTA 2017): <= a href=3D"http://conf.researchr.org/home/issta-2017" target=3D"_blank" data= -saferedirecturl=3D"https://www.google.com/url?hl=3Den&q=3Dhttp://conf.= researchr.org/home/issta-2017&source=3Dgmail&ust=3D1481637234962000= &usg=3DAFQjCNFZoOX1ILSN59w1JbVGGj581rMrHw" style=3D"color: rgb(51, 122,= 183); box-sizing: border-box; text-decoration: none;">http://conf.research= r.org/home/issta-2017. In addition there will be a one-day Rigorous Examination of Reactive Syste= ms verification challenge Workshop (RERS 2017): http://www.rers-challenge.org/2017. An overview of the previous SPIN symposia (and early workshops) can be fou= nd at: http://spinroot.com/spi= n/symposia.

Topics of interest include, but are not limited to:

  • Formal verificatio= n techniques for automated analysis of software
  • Formal analysis for modeling languages, s= uch as UML/state charts
  • Formal specification languages, temporal logic, design-by-contrac= t
  • Model checki= ng
  • Automated t= heorem proving, including SAT and SMT
  • Verifying compilers
  • Abstraction and symbolic execution techniques=
  • Static analys= is and abstract interpretation
  • Combination of verification techniques
  • Modular and compositional verific= ation techniques
  • Verification of timed and probabilistic systems
  • Automated testing using advanced analy= sis techniques
  • Combination of static and dynamic analyses
  • Derivation of specifications, test cases, or = other useful material via formal analysis
  • Case studies of interesting systems or with int= eresting results
  • Engineering and implementation of software verification and analysis too= ls
  • Benchmark a= nd comparative studies for formal verification and analysis tools
  • Formal methods educatio= n and training
  • Insightful surveys or historical accounts on topics of relevance to the sy= mposium
Submission Guidelines

The contributions to SPIN 2017 will be published as ACM Proceedings, and sh= ould be submitted in the ACM Conference Format: https://www.acm.o= rg/publications/proceedings-template.

With the exception of survey and history papers, submissions must be origin= al and should not have been published previously or be under consideration = for publication while being evaluated for this symposium. 

We are soliciting two categories of papers:

  • Full Research Papers describing fully= developed work and complete results (10 pages);
  • Papers should be submitted via the EasyChair SPIN 2017 submission website:&= nbsp;https://easychair.org/conferences/?conf=3Dspin2017.

    Best Paper awards w= ill be given and announced at the conference. 

    A selection of papers will be invited to a special issue of the International Journal on Software Tools for= Technology Transfer (STTT).

    Important Dates
    • Paper Submission: = February 10, 2017 (23:59:59 Anywhere on Earth)
    • Aut= hor Notification : April 15, 2017
    • Camera-Ready Paper: May 20, 2017
    • Symposium : July 13-14, 2017
    Organization
    • Hakan Erdogmus,&nb= sp;Program Co-Chair, Car= negie Mellon University, USA
    • Klaus Havelund, Program Co-Chair, NASA/Caltech Jet Propulsion Laboratory, USA
    • Corina Pasarean= u, Awards Chair, NA= SA Ames Research Center, USA
    • Yli=E8s Falcone, Publicity Chair, Univ. Grenoble Alpes, Inria, France
    Program Committee
    • Erika Abraham, RWT= H Aachen University, Germany
    • Christel Baier, Technical University of Dresden, Germany
    • Tom Ball, Microso= ft Research, USA
    • Ezio Bartocci, Vienna University of Technology, Austria
    • Dirk Beyer, Ludwig-Maximilians= -Universit=E4t M=FCnchen (LMU Munich), Germany
    • Armin Biere, Johannes Kepler University, A= ustria
    • Dragan = Bosnacki, Eindhoven University of Technology, Netherlands
    • Zmago Brezocnik, University of = Maribor, Slovenia
    • Sagar Chaki, Software Engineering Institute CMU, USA
    • Alessandro Cimatti, Fondazione B= runo Kessler, Italy
    • Lucas Cordeiro, University of Oxford, UK
    • Patrice Godefroid, Microsoft Research, USA=
    • Susanne Graf,= VERIMAG Laboratory, France
    • Radu Grosu, Vienna University of Technology, Austria
    • Arie Gurfinkel, Univer= sity of Waterloo, USA
    • Gerard Holzmann, NASA/Caltech Jet Propulsion Laboratory, USA
      • Sarfraz Khurshid, Th= e University of Texas at Austin, USA
    • Kim Larsen, Aalborg University, Denmark
    • Stefan Leue, University of= Konstanz, Germany
    • Alice Miller, University of Glasgow, Scotland
    • Corina Pasareanu, NASA Ames Research C= enter, USA
    • Dor= on Peled, Bar Ilan University, Israel
    • Neha Rungta, NASA Ames Research Center, USA
      • Theo Ruys, RUwise, Ne= therlands
    • Scot= t Smolka, Stony Brook University, USA
    • Scott Stoller, Stony Brook University, United State= s
    • Jun Sun, Sin= gapore University of Technology and Design, Singapore
    • Oksana Tkachuk, NASA Ames Research = Center, USA
    • St= avros Tripakis, University of California, Berkeley, USA
    • Willem Visser, Stellenbosch Unive= rsity, South Africa
    • Farn Wang, National Taiwan University, Taiwan
    • Michael Whalen, University of Minneso= ta, USA
    • Anton = Wijs, Eindhoven University of Technology, Netherlands
    Steering Committee
    • Dragan Bosnacki, E= indhoven University of Technology, Netherlands
    • Susanne Graf, Verimag, France
    • Gerard Holzmann, NASA/Calt= ech Jet Propulsion Laboratory, United States
    • Stefan Leue, University of Konstanz, Germany=
    • Willem Visser= , Stellenbosch University, South Africa
--_000_D473EDDF16B59klaushavelundjplnasagov_-- --===============5389873631686806501== Content-Type: text/plain; charset="us-ascii" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Disposition: inline --- To opt-out from this mailing list, send an email to fm-announcements-request@lists.nasa.gov with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting fm-announcements-owner@lists.nasa.gov --===============5389873631686806501==--