8th LASER Summer School on Software Engineering
|Home | Topics | Speakers | Lectures | Schedule | Other activities | Visitor Info | Contacts | Registration | Previous sessions|
Information will be filled in as soon as it is available.
Speaker: Christine Paulin-Mohring, Université Paris Sud
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).
Speaker: César Muñoz, NASA Langley Research Center
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:
Speaker: Patrick Cousot, École Normale Supérieure
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:
Speaker: Rustan Leino, Microsoft Research
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:
Speaker: Bertrand Meyer, ETH Zurich and Eiffel Software
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:
Speaker: Patrice Godefroid, Microsoft Research
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.
Speaker: Edmund Clarke, Carnegie Mellon
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.
|Chair of Software Engineering - ETH Zurich||Last update: 12.08.2011|