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
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
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
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
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
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
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.30-12: Reasoning Methodology
K. Rustan M. Leino and Nadia Polikarpova.
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
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.
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)
9-10AM: Sandrine Blazy (Rennes University)
A tutorial on the CompCert verified compiler
Compilers are complicated pieces of software that sometimes contain bugs causing wrong executable code to be silently generated from correct source programs. In turn, this possibility of compiler-introduced bugs diminishes the assurance that can be obtained by applying formal methods to source code. This talk gives an overview of the CompCert project: an ongoing experiment in developing and formally proving correct a realistic, moderately-optimizing compiler from a large subset of C to popular assembly languages. The correctness proof, mechanized using the Coq proof assistant, establishes that the generated assembly code behaves exactly as prescribed by the semantic of the C source, eliminating all possibilities of compiler-introduced bugs and generating unprecedented confidence in this compiler. For more about CompCert, please visit http://compcert.inria.fr
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
VSTTE 2013 >