From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id C93E1BC37 for ; Tue, 13 Oct 2009 17:03:58 +0200 (CEST) X-IronPort-AV: E=Sophos;i="4.44,551,1249250400"; d="scan'208";a="48523201" Received: from lri4-102.lri.fr (HELO [129.175.4.102]) ([129.175.4.102]) by mail4-relais-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 13 Oct 2009 17:03:58 +0200 Message-ID: <4AD4977B.3040108@lri.fr> Date: Tue, 13 Oct 2009 17:06:35 +0200 From: =?ISO-8859-1?Q?Jean-Christophe_Filli=E2tre?= User-Agent: Thunderbird 2.0.0.23 (X11/20090817) MIME-Version: 1.0 To: caml-list Subject: Call for Participation: VSTTE 2009 X-Enigmail-Version: 0.96.0 OpenPGP: url=http://www.lri.fr/~filliatr/mykey.asc Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; filliatre:01 filliatre:01 lri:01 eindhoven:01 lri:01 annotations:01 thorsten:01 cuoq:01 smt:01 solvers:01 solver:01 model:01 2009:98 2009:98 19.:98 ********************************************************* * * * VSTTE 2009 * * * * Workshop on Verified Software * * Theory Tools and Experiments * * (affiliated with Formal Methods Week) * * * * *** Call For Participation *** * * * * November 2, 2009 * * Eindhoven, the Netherlands * * http://vstte09.lri.fr/ * * * ********************************************************* The workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 2009) will take place on November the 2nd. The focus of this workshop will be on tools, as previous VSTTE conferences in Zurich and Toronto emphasised theories and experiments. Consisting of contributed papers and invited talks, the workshop will focus on the tools behind the development of systematic methods for specifying, building, and verifying high-quality software. Program ======= 09:00-10:00 - Rajeev Joshi, NASA JPL US TBA 10:30-11:30 - Discovering Specifications for Unknown Procedures with Separation Logic Chenguang Luo, Florin Craciun, Shengchao Qin, Guanhua He and Wei-Ngan Chin. On Essential Program Annotations and Completeness of Verifying Compilers Bernhard Beckert, Thorsten Bormer and Vladimir Klebanov. 11:30-12:30 - Jim Woodcock, University of York UK TBA 13:30-14:30 - Pascal Cuoq, CEA France TBA 14:30-15:30 - SMT Solvers: New Oracles for the HOL Theorem Prover Tjark Weber. An Interval-based SAT Modulo ODE Solver for Model Checking Nonlinear Hybrid Systems Daisuke Ishii, Kazunori Ueda and Hiroshi Hosobe. 16:00-17:00 - John McDermott, Naval Research Lab US TBA Kalou Cabrera Castillos, INRIA Nancy France TBA Registration ============ Participants can register for any combination of FM2009 activities, inclusing VSTTE 2009, at http://www.win.tue.nl/fmweek/Registration.html Deadline for (normal) registration is October 19.