Software Verification

Lyon, January 9-12, 2012

Abstract Interpretation

Click here to get the slides

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.

Automata-Theoretic Model Checking of Reactive Systems

Click here and there to get the slides

Objectives:

Many major hardware (Intel, IBM) and software (Microsoft) companies are now using the technique of Model Checking in practice. Examples of its use include the verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms. The works of A. Pnueli, E. Clarke, E.A Emerson and J. Sifakis on algorithmic verification of systems using the Model Checking has been awarded the 1996 and 2007 Turing awards. The basis of this work is the relation of logic with automata theory, which was introduced by the seminal works of Buechi (1960) and Rabin (1969). This course is intended to introduce the student to the theory and applications of Model Checking.

Syllabus:

1. Classical first- and second-order logic, finite word and tree automata, closure properties and language emptiness.
2. Relationship between Weak Monadic Second-Order Logic and finite automata. Infinite automata on words (Buechi, Mueller) and on trees (Rabin) automata, and their relationship with Monadic Second-Order Logic.
3. LTL Model Checking and Applications

Méthodes de Test du Logiciel

Click here to get the slides

Buts:

Dresser un panorama des méthodes actuelles du test de logiciel, notamment donner des repères pour se retrouver dans la terminologie abondante du domaine ; montrer ce qui est facilement automatisable à l'heure actuelle (état de la technique); montrer quelques méthodes avancées d'automatisation du test (état de l'art).

Nous nous attacherons à bien distinguer le cas des systèmes embarqués de celui de programmes plus standards, et à distinguer les procédures de test réalisées dans un cadre de certification (systèmes critiques) des procédures de test usuelles.

Points abordés :

1. Terminologie / background
   • Processus de test
   • Typologie des différentes familles de test
   • Place dans le cycle de développement du logiciel
   • Points difficiles
2. Méthodes de sélection de test
   • Interface testing
   • Test aléatoire / statistique
   • Couverture structurelle
   • Mutations
3. Automatisation, état de la technique : tests de régression
   • Rejeu, maintenance (ex : JUnit)
   • Sélection / minimisation / prioritisation
4. Automatisation, état de l'art 1 : exécution dynamique symbolique (ex : Pex et Sage chez Microsoft)
5. Automatisation, état de l'art 2 : model-based testing

Mechanized semantics with applications to compiler verification

Click here to get the supports (slides and programs)

Abstract

The goal of this lecture is to show how modern theorem provers -- I use the Coq proof assistant -- can be used to mechanize the specification of programming languages and their semantics, and to reason over individual programs as well as over generic program transformations, as typically found in compilers.

The topics covered include:

1. Operational semantics: small-step, big-step, definitional interpreters.
2. Compilation to virtual machine code and its proof of correctness.
3. Examples of program optimizations: dead code elimination, register allocation.
4. Compiler verification "in the large" : an overview of the CompCert verified C compiler.