This website is about the 2011 edition of the school. Visit this year's edition of LASER.

8th LASER Summer School on Software Engineering

 

Tools for Practical Software Verification

September 4-10, 2011 - Elba Island, Italy

Edmund Clarke (Carnegie Mellon)
Patrick Cousot (École Normale Supérieure)
Patrice Godefroid (Microsoft Research)
Rustan Leino (Microsoft Research)
Bertrand Meyer (ETH Zurich)
César Muñoz (NASA Langley Research Center)
Christine Paulin-Mohring (Université Paris-Sud)
Andrei Voronkov (University of Manchester)

 
   
 

Lectures

Information will be filled in as soon as it is available.

The Coq proof assistant

Speaker: Christine Paulin-Mohring, Université Paris Sud

Description:

Coq is a proof assistant, that is an interactive environment where the user can define objects and prove theorems. Examples of uses of Coq includes a formal proof of the 4-colors theorem, a formally verified compiler for the C language, environments to reason on the JavaCard platform, and cryptographic programs.

Objects in Coq are either concrete data such as integers and trees, or abstract notions such as sets and relations or inductively defined logical properties. They are defined in the Coq language which includes both an higher-order typed functional language and inductive and co-inductive definitions. Coq provides high-level tools to build proofs of properties; a proof is translated into a concrete term which is checked by a trusted kernel, making Coq one of the safest tools for doing proofs on computer. From a Coq development, it is also possible to extract an Ocaml or Haskell program which, by construction, will be correct with respect to the specification given and proven in Coq.

The course will cover basic aspects of the language ((co)-inductive definitions, functional programming with dependent types, modules) and the proof environment (tactics).

References :

  • The Coq proof assistant http://coq.inria.fr (software and documentation)
  • Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions. Series: Texts in Theoretical Computer Science. An EATCS Series 2004.

Short biography:
see Speakers page



Advanced Theorem Proving Techniques in PVS with Applications

Speaker: César Muñoz, NASA Langley Research Center

Description:

PVS (Prototype Verification System) [http://pvs.csl.sri.com] is an interactive environment for the specification and verification of systems. PVS provides a strongly typed specification language, which is based on Higher-Order Logic. The type system of PVS supports: sub-typing, dependent-types, abstract data types, parametric types, records, unions, and tuples. The PVS theorem prover includes decision procedures for a variety of theories such as linear arithmetic, propositional logic, and temporal logic. The Formal Methods group at NASA Langley develops and applies PVS theorem proving technology for verification of safety-critical aerospace applications. This seminar will provide a gentle introduction to advanced PVS features, including: theory interpretations, real number proving, non-linear arithmetic, implicit induction, batch proving, rapid prototyping, and strategy development. All of these features are illustrated with examples taken from verification research at NASA.

Material:

Short biography:
see Speakers page



Abstract interpretation based tool construction for software verification

Speaker: Patrick Cousot, École Normale Supérieure

Description:

We will show how tools for software verification such as SMT solver and theorem prover based verfiers (where the inductive argument necessary for the proof is either provided by the end-user or by refinement of the specification such as code contracts) or static analyzers (where the inductive argument necessary for the proof is computed directly (e.g. by elimination) or iteratively with convergence acceleration by widening/narrowing) can be constructed by systematic abstraction of their transition-based or structural operational semantics thus leading to verified verification tools. As an application, we will consider the construction of static analyzers for proving program safety properties. Examples such as ASTRÉE will be rapidly overviewed.

Material:

Short biography:
see Speakers page



Using and building an automatic program verifier

Speaker: Rustan Leino, Microsoft Research

Description:

A program verification tool can help construct reliable software. These lectures start with a tutorial on using a modern program verifier, and then turn to a recipe for building your own program verifier.

Exercises:

Short biography:
see Speakers page

Verification As a Matter Of Course

Speaker: Bertrand Meyer, ETH Zurich and Eiffel Software

Description:

Software verification techniques should not remain the apanage of a small set of developers of life-endangering systems, but can benefit software development of almost any kind. To provide this benefit, they must: (1) become a normal, unobtrusive part of software development, in the same way as (for example) static type checking; (2) integrate well with modern processes and practices of software development, rather than disrupting established, proven practices; (3) integrate well with a modern IDE, through close coupling with its other constituents such as the compiler, the editor, the browser, the debugger and other facilities; (4) handle modern programming languages, in particular the full extent of object-oriented methods; (5) particularly, handle references (pointers) and complex data structures; (6) scale up to large programs; (7) combine all applicable verification methods, including static methods (proofs) and dynamic ones (test).

This series of lectures will describe such a comprehensive verification environment under construction (EVE, the Eiffel Verification Environment), with particular emphasis on verifying object-oriented programs working on linked data structures. The plan of the lectures is as follows:

  1. EVE and Verification As a Matter Of Course: an overview.
  2. Handling references (1): the alias calculus
  3. Compositional logic
  4. Handling references (2): the calculus of object structures
  5. Automated testing: AutoTest
  6. Further developments

References

Short biography:
see Speakers page

Software Model Checking via Systematic Testing

Speaker: Patrice Godefroid, Microsoft Research

Description:

Model checking and testing have a lot in common. Over the last two decades, significant progress has been made on how to broaden the scope of model checking from finite-state abstractions to actual software implementations. One way to do this consists of adapting model checking into a form of systematic testing that is applicable to industrial-size software. The aim of these lectures is to present a comprehensive overview of this strand of software model checking, by describing the main ideas, techniques and results obtained in this area, including combinations with static program analysis.

Short biography:
see Speakers page

Model Checking and the Curse of Dimensionality

Speaker: Edmund Clarke, Carnegie Mellon

Description:

The term "Curse of Dimensionality" was coined by the famous mathematician, Richard Bellman. He used the term to describe the exponential increase in volume associated with adding extra dimensions to an object in space. One implication of the Curse of Dimensionality is that methods for numerical solution of various optimization problems require vastly more computer time when the number of state variables involved increases. A similar phenomenon occurs in temporal logic model checking. Model checking is an automatic verification technique for concurrent systems that are finite state or have finite state abstractions. It has been used successfully to verify computer hardware and is beginning to be used to verify computer software as well. As the number of state variables in the system increases, the number of global system states grows exponentially. This is called the “state explosion problem”. Much of the research in model checking over the past 30 years has involved developing techniques for dealing with this problem. In this series of lectures I will explain how the basic model checking algorithms work and describe some recent approaches to the state explosion problem. I will discuss how these techniques can be used to make model checking feasible for computer software and to understand molecular processes in systems biology.

Short biography:
see Speakers page

 

Chair of Software Engineering - ETH Zurich Last update: 12.08.2011