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 (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-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 |

VSTTE 2013 >