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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 5010A7EE51 for ; Thu, 2 May 2013 05:32:27 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of owre@csl.sri.com) identity=pra; client-ip=128.18.84.133; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="owre@csl.sri.com"; x-sender="owre@csl.sri.com"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of owre@csl.sri.com) identity=mailfrom; client-ip=128.18.84.133; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="owre@csl.sri.com"; x-sender="owre@csl.sri.com"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.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=mail3-smtp-sop.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: AvsBAGHdgVGAElSFnGdsb2JhbABSgz6CXVq3WIUVFg4BAQEBAQgLCQkUKIIXGxEGRQUFIBwCBSECEVQBhgKCFgyTTYw4jlyQSRWBDowyCoQJgRMDiReKQ4R1im2IS4FLJA X-IPAS-Result: AvsBAGHdgVGAElSFnGdsb2JhbABSgz6CXVq3WIUVFg4BAQEBAQgLCQkUKIIXGxEGRQUFIBwCBSECEVQBhgKCFgyTTYw4jlyQSRWBDowyCoQJgRMDiReKQ4R1im2IS4FLJA X-IronPort-AV: E=Sophos;i="4.87,593,1363129200"; d="scan'208";a="12929898" Received: from brightmail-internal4.sri.com ([128.18.84.133]) by mail3-smtp-sop.national.inria.fr with ESMTP; 02 May 2013 05:32:25 +0200 X-AuditID: 80125485-b7fd16d00000648e-cc-5181de47482f 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 F0.91.25742.74ED1815; Wed, 1 May 2013 20:32:23 -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 r423WIgH087705 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NO); Wed, 1 May 2013 20:32:18 -0700 (PDT) (envelope-from owre@csl.sri.com) Received: from owre (helo=ubi) by ubi with local-esmtp (Exim 4.76) (envelope-from ) id 1UXkFm-00069P-9Y; Wed, 01 May 2013 20:32:18 -0700 To: Undisclosed recipients: ; X-Mailer: MH-E 8.2; nmh 1.3; GNU Emacs 23.3.1 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Date: Wed, 01 May 2013 20:32:18 -0700 Message-ID: <23646.1367465538@ubi> From: Sam Owre X-Brightmail-Tracker: H4sIAAAAAAAAA02Ra0hTYRzGeT3nbEdpdZyX3jSDRiIa0yTFN8hLfsj3Q5RSkF3QTnlwy3k7 M03pw9QmOQlXRnirZtEyFbWJtMy0Vs0LmFoWGhoomqIZebflNHUIfvs9///D78tDE+JB0o2W J6VxfBKrkAgcyJwEsE8a8SM76tD8qCv6aHwOUHlNO4X6u5OQqvEdQLPGehL9MbRQyNLziULj JZUEqp7vt0OFA6PrNeswgQo754RosreMRHeeZANUYMJoYfq+EM23HUeVYxYCzT37SqGCfx6o YbpSiBb0jyjUNKgXotcrHeuemUk7ZCoiUe+vZkGYO17W9JH4VnsablS3kXhAG4J1H07gTpVO gO8N5RB4eaqOwjXaJYCtr6LxatFjEpvNagJripzw3QkTiUuWjQA3mVuFkXvOOxyN4xTydI73 C7nkIFu7bSVTtMHXTTPVhAo88NMAexoyAbBT+1JoY1fY86NOoAEOtJipsoMtah2wBSuAqx2t lC0UA6izzpIaQNPOjAdc6eY30InxgV3DvE0khautNeQGixhH2FEyuskE4wVXHn4mbHwQ6ium NplkPKGl4SZh60vgt0ELtcECZj/M/V5BaMHO0m2q0m2q0m0qHSCqwN7LvDxelpbIyhXSraUD fJW83PdKcqIBrG+uEp9RG0Fls78JMDSQ7BDNSbOjxBSbrsxMNAFIExJn0Zfu9ZMojs3M4vjk WP6aglOagDtNSnaLFoN2nRIz8Wwal8BxKRy/9bWj7d1UICnfWxoeHtdv6BUvn6x/WhfmfnHo bZfR4F18+ob/77LaRsegHKW57dyF0L+sWB27OB6x6gh+xuTmRrIHalPfh+WBs28ykgNTRS6W 8t66Ppn5cJ5elRqtWWg9NrGWYQ4eUUCXJYNnif6F1xiwGAK7Y2QzzdLOq9r8I9EjoVlZElIp Y/19CF7J/geS14F87wIAAA== 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, 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. Registration: http://fm.csl.sri.com/VSTTE2013/registration.html Note that the Summer School on Formal Techniques follows shortly after at the same location (http://fm.csl.sri.com/SSFT13/) Program: -------- Thur May 16, 2013 6PM: Wine/Cheese Reception Fri May 17, 2013 9-10AM: Alex Aiken (Stanford): Using Learning Techniques in Invariant Inference Abstract: Arguably the hardest problem in automatic program verification is designing appropriate techniques for discovering loop invariants (or, more generally, recursive procedures). Certainly, if invariants are known, the rest of the verification problem becomes easier. This talk presents a family of invariant inference techniques based on using test cases to generate an underapproximation of program behavior and then using learning algorithms to generalize the underapproximation to an invariant. These techniques are simpler, much more efficient, and appear to be more robust than previous approaches to the problem. If time permits, some open problems will also be discussed. 10-10.30AM: Break 10.30-12 noon: Static Analysis Philipp Ruemmer, Hossein Hojjat and Viktor Kuncak. Classifying and Solving Horn Clauses for Verification 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 noon-1.30PM: Lunch 1.30-3PM: Model Checking Pamela Zave and Jennifer Rexford. Compositional Network Mobility 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 3-3.30PM: Break 3.30-4.30PM: Unrolling Tuan-Hung Pham and Michael Whalen. An Improved Unrolling-Based Decision Procedure for Algebraic Data Types Julian Tschannen, Carlo A. Furia, Martin Nordio and Bertrand Meyer. Program Checking With Less Hassle 5-6PM: Panel (TBD) Sat May 18, 2013 9-10AM: Nikhil Swamy (Microsoft Research): F*: Certified Correctness for Higher-order Stateful Programs Abstract: F* is an ML-like programming language being developed at Microsoft Research. It has a type system based on dependent types and a typechecker that makes use of an SMT solver to discharge proof obligations. The type system is expressive enough to express functional correctness properties of typical, higher-order stateful programs. We have used F* in a variety of settings, including in the verification of security protocol implementations; as a source language for secure web-browser extensions; as an intermediate verification language for JavaScript code; to verify the correctness of compilers; as a relational logic for probabilistic programs; and as a proof assistant in which to carry out programming language metatheory. We have also used F* to program the core typechecker of F* itself and have verified that it is correct. By bootstrapping this process using the Coq proof assistant, we obtain a theorem that guarantees the existence of a proof certificate for typechecked programs. I will present a brief overview of the F* project, drawing on the examples just mentioned to illustrate the features of the F* language and certification system. For more about F*, visit http://research.microsoft.com/fstar. 10-10.30: Break 10.30-12: Reasoning Methodology K. Rustan M. Leino and Nadia Polikarpova. Verified Calculations Jean-Christophe Filliatre, Claude March=C3=A9, Fran=C3=A7ois Bobot, And= rei Paskevich and Guillaume Melquiond. Preserving User Proofs Across Specification Changes Daniel Jost and Alexander J. Summers. An automatic encoding of VeriFast Predicates into Implicit Dynamic Frames 12-1.30: Lunch 1.30-2.30: Andre Platzer: How to Explain Cyber-Physical Systems to Your Verifier Abstract: Despite the theoretical undecidability of program verification, practical verification tools have made impressive advances. How can we take verification to the next level and use it to verify programs in cyber-physical systems (CPSs), which combine computer programs with the dynamics of physical processes. Cars, aircraft, and robots are prime examples where this matters, because they move physically in space in a way that is determined by discrete computerized control algorithms. Because of their direct impact on humans, verification for CPSs is even more important than it already is for programs. This talk describes how formal verification can be lifted to one of the most prominent models of CPS called hybrid systems, i.e. systems with interacting discrete and continuous dynamics. It presents the theoretical and practical foundations of hybrid systems verification. The talk shows a systematic approach that is based on differential dynamic logic comes with a compositional proof technique for hybrid systems and differential equations. This approach is implemented in the verification tool KeYmaera and has been used successfully for verifying properties of aircraft, railway, car control, autonomous robotics, and surgical robotics applications. 2.30-3PM: Break 3-5.00PM: System Verification Shilpi Goel and Warren Hunt. Automated Code Proofs on a Formal Model of the X86 Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, 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=A4hl= er and Wolfgang Reif. Verification of a Virtual Filesystem Switch Liang Zou, Jidong Lv, Shuling Wang, Naijun Zhan, Tao Tang, Lei Yuan and Yu Liu. Verifying Chinese Train Control System Under a Combined Scenario by Theorem Proving 5.30-6.30PM: Panel (TBD) 8PM: Banquet 9-10AM: Sandrine Blazy A Tutorial on the CompCert Verified Compiler. 10-10.30: Break 10.30-noon: Verified Tools 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 noon-1.30: Lunch 1.30-5: Excursion