8th LASER Summer School on Software Engineering


Home  Topics  Speakers  Lectures  Schedule  Other activities  Visitor Info  Contacts  Registration  Previous sessions  
LecturesInformation will be filled in as soon as it is available. The Coq proof assistant
Speaker: Christine PaulinMohring, 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 4colors 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 higherorder typed functional language and inductive and coinductive definitions. Coq provides highlevel 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 :
Short biography: Advanced Theorem Proving Techniques in PVS with Applications
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 HigherOrder Logic. The type system of PVS supports: subtyping, dependenttypes, 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 safetycritical aerospace applications. This seminar will provide a gentle introduction to advanced PVS features, including: theory interpretations, real number proving, nonlinear 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: Abstract interpretation based tool construction for software verification
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 enduser 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 transitionbased 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: Using and building an automatic program verifier
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:
Short biography: Verification As a Matter Of Course
Speaker: Bertrand Meyer, ETH Zurich and Eiffel Software Software verification techniques should not remain the apanage of a small set of developers of lifeendangering 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 objectoriented 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 objectoriented programs working on linked data structures. The plan of the lectures is as follows:
References Short biography: Software Model Checking via Systematic Testing
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 finitestate 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 industrialsize 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: Model Checking and the Curse of Dimensionality
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. Short biography: 
Chair of Software Engineering  ETH Zurich  Last update: 12.08.2011 