VSTTE 2013 Call for Participation

[Sam Owre]

                     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é, François Bobot, Andrei
    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örg Pfähler 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é Maroneze and David Pichardie.
          Formal Verification of Loop Bound Estimation for WCET Analysis
    Frédéric 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