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 5ADA37EE51 for ; Tue, 23 Apr 2013 23:18:32 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of owre@csl.sri.com) identity=pra; client-ip=128.18.84.133; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="owre@csl.sri.com"; x-sender="owre@csl.sri.com"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of owre@csl.sri.com) identity=mailfrom; client-ip=128.18.84.133; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="owre@csl.sri.com"; x-sender="owre@csl.sri.com"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@brightmail-internal4.sri.com) identity=helo; client-ip=128.18.84.133; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="owre@csl.sri.com"; x-sender="postmaster@brightmail-internal4.sri.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjICAMP5dlGAElSFnGdsb2JhbABQgzyCV1q3A4UfFg4BAQEBAQgLCQkUKIIXGxEGRSocAgUhAhFUAYYCgh4MkHuMNI5TgkCPKAQVgQ6MOIQKgRMDiQ+iVoFMJA X-IPAS-Result: AjICAMP5dlGAElSFnGdsb2JhbABQgzyCV1q3A4UfFg4BAQEBAQgLCQkUKIIXGxEGRSocAgUhAhFUAYYCgh4MkHuMNI5TgkCPKAQVgQ6MOIQKgRMDiQ+iVoFMJA X-IronPort-AV: E=Sophos;i="4.87,537,1363129200"; d="scan'208";a="14572414" Received: from brightmail-internal4.sri.com ([128.18.84.133]) by mail2-smtp-roc.national.inria.fr with ESMTP; 23 Apr 2013 23:18:30 +0200 X-AuditID: 80125485-b7fd16d00000648e-0c-5176faa492fe Received: from mx0.csl.sri.com (mx0.csl.sri.com [130.107.1.30]) (using TLS with cipher AES256-SHA (AES256-SHA/256 bits)) (Client did not present a certificate) by brightmail-internal4.sri.com (SRI Internal SMTP Gateway) with SMTP id 89.55.25742.4AAF6715; Tue, 23 Apr 2013 14:18:28 -0700 (PDT) Received: from ubi (ubi.csl.sri.com [130.107.15.8]) by mx0.csl.sri.com (8.14.3/8.14.2) with ESMTP id r3NLGtYe097813 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO); Tue, 23 Apr 2013 14:17:25 -0700 (PDT) (envelope-from owre@csl.sri.com) Received: from owre (helo=ubi) by ubi with local-esmtp (Exim 4.72) (envelope-from ) id 1UUka7-0007mm-5W; Tue, 23 Apr 2013 14:16:55 -0700 To: Undisclosed recipients: ; X-Mailer: MH-E 8.2; nmh 1.3; GNU Emacs 23.1.1 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Date: Tue, 23 Apr 2013 14:16:55 -0700 Message-ID: <29931.1366751815@ubi> From: Sam Owre X-Brightmail-Tracker: H4sIAAAAAAAAA02Ra0hTYRzGeXcuO0qr49R8Wxk2KEPTkoReuohCxPtBMMMgFMqVJzfcppwt UfvQtJSahbOF6JRSyzUvZBiCtyyHeYO8BNYMkwTNcBlTZy6dkroEv/2e5w+//4eHIcSjpIRR qLUcr5YppbQ3mZcGDoa9WMmMP9H9+TT60FILkG1IjXTNXQAttLwmkaOpk0Irw4MUmimzEKje aROgorEpCtnWJglUNLAoRLMj5SQqfp4LUKEVo6W5EiFy9l5AlukVAi2+HKVQ4WogejNnEaIl 8zMKtY2bhajd3b/hmZ8VIKuRRCO/OuhoCb7fp8XN+b0kHjNE4cruWDygq6Txk295BHbZGync YFgGeK31Cl43VpO4pyefwHqjL37800riMlcLwG0974S4vXJRcBEmep9N4ZSKTI4/HpXsLTd0 38ywHcqyT02TOuCS6IEXA9lIaGyoIz28Fw5PNNJ64M2I2ToBnJqoEHjCOoBd7pr/oRTAmfo+ Sg8Yxo8NhO4hfhN92RD4cZL3iMLgfHWZcJNFrA/sL5vaekCwwdD99BPh4VBorrJvMckehhOl nWBTI2Kl0O2mN2uaPQTvfq0iDGC3aYfJtMNk2mGqBEQdOHCdV6TKtSqZQhm2PXFkuIZXhN9I VzWBjbF14oT8FmDpiLAClgHSXSK7KTNeTMkyNdkqK4AMIfUTnSnfqEQpsuwcjk+/xt9Schor 2M+Q0gDRn1N74sRsqkzLpXFcBsdvXwWMl0QHtGRQI5Eax5f433Zk0e+7ucYFzaDz3sCyKuA3 DJENxLQniboWCuL81cEdjooqQ4w5+tXJ0vlzrrfxd2r28eePOJNXix+mj/iE9F+lOpWtiUuO S5eP5eSGBVXngUe5f0vkCYacwtgHScH+ha1NRyPGB78g+ntK64/Qgs7aHLpeSmrksogQgtfI /gEgLcvp6AIAAA== Subject: [Caml-list] VSTTE 2013 Call for Participation CALL FOR PARTICIPATION Fifth Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2013) May 17--19, 2013, Menlo College, Atherton, California [https://sites.google.com/site/vstte2013/] The Fifth IFIP Working Conference on Verified Software: Theories, Tools, and Experiments follows a successful inaugural working conference at Zurich in 2005 followed by conferences in Toronto (2008), Edinburgh (2010), and Philadelphia (2012). The goal of this conference is to advance the state of the art in the science and technology of software verification, through the interaction of theory development, tool evolution, and experimental validation. Invited speakers: Alex Aiken (Stanford), Sandrine Blazy (Rennes), Nikhil Swamy (Microsoft), Andre Platzer (CMU) Accepted papers: Daniel Jost and Alexander J. Summers. An automatic encoding of VeriFast Predicates into Implicit Dynamic Fram= es Philipp Ruemmer, Hossein Hojjat and Viktor Kuncak. Classifying and Solving Horn Clauses for Verification Tuan-Hung Pham and Michael Whalen. An Improved Unrolling-Based Decision Procedure for Algebraic Data Types Olivier Bouissou, Eric Goubault, Sylvie Putot, Jean Goubault-Larrecq and = Assale Adje. Static Analysis of Programs with Imprecise Probabilistic Inputs Etienne Kneuss, Viktor Kuncak and Philippe Suter. Effect Analysis for Programs with Callbacks K. Rustan M. Leino and Nadia Polikarpova. Verified Calculations=20=20=20 Jean-Christophe Filliatre, Claude March=C3=A9, Fran=C3=A7ois Bobot, Andre= i Paskevich and Guillaume Melquiond. Preserving User Proofs Across Specification Changes=20=20=20 Pamela Zave and Jennifer Rexford. Compositional Network Mobility Julian Tschannen, Carlo A. Furia, Martin Nordio and Bertrand Meyer. Program Checking With Less Hassle Nicolas Rosner, Carlos Gustavo Lopez Pombo, Nazareno Aguirre, Ali Jaoua, = Ali Mili and Marcelo Frias. Parallel Bounded Verification of Alloy Models by TranScoping Stephan Falke, Florian Merz and Carsten Sinz. Extending the Theory of Arrays: memset, memcpy, and Beyond Sandrine Blazy, Andr=C3=A9 Maroneze and David Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis Fr=C3=A9d=C3=A9ric Besson, Pierre-Emmanuel Cornilleau and Thomas Jensen. Result Certification of Static Program Analysers with Automated Theorem= Provers Anthony Narkawicz and Cesar Munoz. A Formally Verified Generic Branching Algorithm for Global Optimization Shilpi Goel and Warren Hunt. Automated Code Proofs on a Formal Model of the X86 Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bour= ke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein. seL4: from General Purpose to a Proof of Information Flow Enforcement Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, J=C3=B6rg Pf=C3=A4hler= and Wolfgang Reif. Verification of a Virtual Filesystem Switch Liang Zou, Jidong Lv, Shuling Wang, Naijun Zhan, Tao Tang, Lei Yuan and Y= u Liu. Verifying Chinese Train Control System Under a Combined Scenario by The= orem Proving School/Workshops: The conference will be colocated with the Third Summer School on Formal Techniques, and is preceded by NFM 2013 at NASA Ames and followed by ICSE 2013 at San Francisco. Conference Chair: Natarajan Shankar, SRI International Program Chairs: Ernie Cohen, Microsoft, Andrey Rybalchenko, TU Munich=20 Program Committee: Josh Berdine, Ahmed Bouajjani, Marsha Chechik, Jean-Christophe Filliatre, Silvio Ghilardi, Aarti Gupta, Arie Gurfinkel, Andrew Ireland, Ranjit Jhala, Cliff Jones, Rajeev Joshi, Gerwin Klein, Daniel Kroening, Gary Leavens, Xavier Leroy, Zhiming Liu, Pete Manolios, Tiziana Margaria, David Monniaux, Peter Mueller, David Naumann, Aditya Nori , Peter O'Hearn, Matthew Parkinson, Wolfgang Paul, Andreas Podelski, Zhang Shao, Willem Visser, Thomas Wies, Jim Woodcock, Kwangkeun Yi, Pamela Zave, Lenore Zuck Publicity Chair: Sam Owre, SRI International Steering Committee: Tony Hoare, Andrew Ireland, Jay Misra, Natarajan Shankar, Jim Woodcock