Programme

Planning

• Lundi 25
  • 14h - 17h30: Coccinelle: Practical program transformation for the Linux kernel (Julia Lawall)
    
• Mardi 26
  
  • 9h - 12h: Interprétation abstraite et propriétés de programmes C (Virgile Prevosto)
  • 13h - 16h:  Etude Empirique En Génie Logiciel – Application sur GitHub et Alexa (Xavier Blanc)
• Mercredi 27
  
  • 9h - 12h30: Introduction to Certified Software Development in Coq  (Matthieu Sozeau)
  • 14h - 17h30: Introduction à la programmation par contraintes (Charlotte Truchet)
• Jeudi 28
  
  • 9h - 11h45: Verification of security protocols: from confidentiality to privacy (Stéphanie Delaune)
  • 11h45 - 15h15:  Software Variability and Artificial Intelligence (Mathieu Acher)
  • 15h40 Visite du Musée des Confluences
    
  • 20h00 Dîner    
    Restaurant Le caro de Lyon, 25 rue du Bât d'Argent - 69001 Lyon
    (métro Cordeliers si on vient de Perrache, Hôtel de Ville si on vient de Charpennes)
• Vendredi 29
  
  • 9h - 12h30: Deductive Program Verification with Why3 (Andrei Paskevich)

Titres et descriptifs des cours

Les transparents sont disponibles sur la page Supports de cours 

Lundi 25 juin après-midi 

  Julia Lawall Coccinelle: Practical program transformation for the Linux kernel

 Coccinelle is a program matching and transformation tool for C code that has been developed with the goal of performing source code evolutions and finding bugs in the Linux kernel. Coccinelle has been used in contributing to the Linux kernel for over 10 years and has supported the development of thousands of kernel patches. It can also be useful for more general C code processing tasks. In this talk, we will provide an overview of Coccinelle and its use in the Linux kernel. Exercises will be included.

Participants should download the source code of Linux 3.2 and Coccinelle:

Linux kernel:
git clone
https://kernel.googlesource.com/pub/scm/linux/kernel/git/torvalds/linux
cd linux
git checkout v3.2

Coccinelle: http://coccinelle.lip6.fr/download.php

 

Mardi 26 juin matin

  Virgile Prevosto: Interprétation abstraite et propriétés de programmes C

L'interprétation abstraite est une technique d'analyse de programmes introduite par Patrick et Radhia Cousot en 1977. Elle se place dans le cadre général des analyses flot de données, où l'on propage des informations le long des arêtes du graphe de flot de contrôle d'un programme, jusqu'à atteindre un point fixe, où il n'est plus possible d'ajouter de l'information à celle déjà associée à chacun des nœuds du graphe par les opérations précédentes.

Dans ce contexte, le but de l'interprétation abstraite est de remplacer l'ensemble des exécutions concrètes possibles d'un programme par une seule exécution abstraite, qui propage une abstraction des états concrets pouvant atteindre les nœuds correspondants. D'un point de vue théorique, l'interprétation abstraite repose sur deux ingrédients fondamentaux. Tout d'abord, la notion d'insertion de Galois permet de donner une condition assez simple pour que l'abstraction soit correcte, c'est à dire que les états abstraits représentent bien une surapproximation de l'ensemble des états concrets possibles. Par ailleurs, l'opérateur d'élargissement permet de garantir que l'analyse termine toujours, même sur des programmes ayant des boucles infinies.

Le cours présentera rapidement les principes de base de l'interprétation abstraite, et montrera comment ceux-ci sont mis en œuvre au sein du greffon EVA de l'outil Frama-C pour vérifier l'absence de comportement indéfinis dans les programmes C, et plus généralement pour obtenir une surapproximation des valeurs possibles de chaque location mémoire en chaque point de programme. En particulier, à travers différents exemples de code C, on examinera les différents moyens de configurer l'analyseur pour obtenir le meilleur compromis entre temps d'exécution de l'analyseet précision des résultats obtenus.

Mardi 26 juin après-midi

  Xavier Blanc: Etude Empirique En Génie Logiciel – Application sur GitHub et Alexa     

La recherche en génie logiciel vise essentiellement à optimiser la  production et la maintenance logicielle. Dans un tel contexte, les  études empiriques permettent de vérifier la plus-value d’approches  proposées. Le principe général est de définir une hypothèse de  plus-value et de la confronter à des mesures statistiques réalisées sur  des projets existants.  Ce cours présentera les différentes méthodes employées pour réaliser des  études empiriques. Il illustrera ces méthodes en montrant les résultats  obtenus ces dernières années. Enfin, une application sera présentée en  prenant comme cible d’observation les projets open source dans GitHub ou  les applications web populaires listées par Alexa.

Mercredi 27 juin matin

  Matthieu Sozeau: Introduction to Certified Software Development in Coq   

This lecture will be an introduction to the Coq proof assistant and its use for the verification of programs and proofs (actually, they're the  same thing!). The Coq system is based on Type Theory, which acts as a  kind of formal logic and is at the same time a purely functional  programming language in its own right (this link is the so-called  Curry-Howard isomorphism). As such, Coq is a general purpose theorem prover that can be used to formalize mathematical proofs, including  proofs about the semantics of programming languages, or proofs about  computer software and systems. For example, semantic-based tools on programming languages like type checkers, compilers or static analysers  can be implemented in the programming language of Coq and verified in  the same language, with a high degree of confidence. We will give an  informal overview of the logic and the computational programming  language and its applications, focusing in particular on what this  isomorphism means in practice. Of course, interactive theorem proving is  a non-trivial activity, as the user and the program interact to build  proofs of theorems well outside the reach of automated deduction. I will  give a glimpse of how this happens in practice and why it can become a somewhat addictive game.

Mercredi 27 juin après-midi

  Charlotte Truchet: Introduction à la programmation par contraintes 

La programmation par contraintes s’attache à résoudre des problèmes  fortement combinatoires, exprimés à l’aide de relations logiques (les  contraintes), portant sur des variables dans des domaines fixés, souvent  finis. Chaque type de contraintes est dotée d’un algorithme de  propagation, qui élague autant que possible les domaines des variable sans perdre de solutions. Les solveurs appliquent ces propagateurs tant  que c’est possible, puis effectuent des choix (affectation d’une valeur à une variable, réduction d’un domaine) et itèrent le processus. On sait  aujourd’hui résoudre des familles de contraintes assez larges (cardinalité, graphes, mots, géométrie…). Dans ce cours, je présenterai  les notions principales du domaine (contraintes, domaines, consistance,  propagation, heuristiques) puis j’introduirai un format générique pour  représenter les domaines et les consistances, basé sur la notion de  domaine abstrait telle que définie en interprétation abstraite, ainsi  qu’une méthode de résolution générique sur ces nouveaux domaines. On  détaillera l’exemple du domaine des octogones.

Jeudi 28 juin matin

  Stéphanie Delaune: Verification of security protocols: from confidentiality to privacy

Security protocols are widely used today to secure transactions that take place through public channels like the Internet. Typical functionalities are the transfer of a credit card number or the authentication of a user on a system. Because of their increasing ubiquity in many important applications (e.g. electronic commerce, smartphone, government-issued ID . . . ), a very important research challenge consists in developing methods and verification tools to increase our trust on security protocols, and so on the applications that rely on them. 

Formal methods offer symbolic models to carefully analyse security protocols, together with a set of proof techniques and efficient tools such as ProVerif. These methods build on techniques from model-checking, automated reasoning and concurrency theory. We will explain how security protocols as well as the security properties they are supposed to achieve are formalised in symbolic models. Then, we will describe and discuss some techniques to automatically verify different kinds of security properties

Jeudi 28 juin après-midi

  Mathieu Acher: Software Variability and Artificial Intelligence

Most modern software systems are subject to variation or come in many variants. Web browsers like Firefox or Chrome are available on different operating systems, in different languages, while users can configure 2000+ preferences or install numerous 3rd parties extensions (or plugins). Web servers like Apache, operating systems like the Linux kernel, or a video encoder like x264 are other examples of software systems that are highly configurable at compile-time or at run-time for delivering the expected functionality andmeeting the various desires of users.

Variability ("the ability of a software system or artifact to be efficiently extended, changed,customized or configured for use in a particular context") is therefore a crucial property of software systems. Organizations capable of mastering variability can deliver high-quality variants (or products) in a short amount of time and thus attract numerous customers, new use-cases or usage contexts. A hard problem for end-users or software developers is to master the combinatorial explosion induced by variability: Hundreds of configuration options can be combined, each potentially with distinct functionality and effects on execution time, memory footprint, quality of the result, etc. The first part of this course will introduce variability-intensive systems, their applications and challenges, in various software contexts. We will use intuitive examples (like a generator of LaTeX paper variants) and real-world systems (like the Linux kernel).

A second objective of this course is to show the relevance of ArtificialIntelligence (AI) techniques for exploring and taming such enormous variability spaces. In particular, we will introduce how (1) satisfiability and constraint programming solvers can be used to properly model and reason about variability; (2) how machine learning can be used to discover constraints and predict the variability behavior of configurable systems or software product lines.

Vendredi 29 juin matin

  Andrei Paskevich Deductive Program Verification with Why3

This lecture is an introduction to deductive program verification and a tutorial on the Why3 tool. Why3 provides a programming language with specification annotations, type polymorphism, mutable data types, algebraic data types, pattern matching, and exceptions. It allows us to verify annotated programs using automated and interactive theorem provers like Alt-Ergo, CVC4, Z3, Coq, and many others. This lecture introduces elementary concepts and techniques of program verification: pre- and postconditions, loop invariants, ghost code, termination proofs, modeling of data structures, etc.