Programme

 

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.

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.

Xavier Blanc
Étude 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.

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 zone 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’analyse et précision des résultats obtenus.

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.

Assia Mahboubi
Introduction à la preuve formelle avec Coq

• Ce cours propose une introduction à la pratique des preuves formelles en théorie des types dépendants, à l’aide d’un assistant de preuve interactif et de ses bibliothèques. Ces outils permettent d’écrire des bibliothèques numériques de mathématiques formalisées. Ils sont utilisés aussi bien pour des applications en informatique, en particulier pour vérifier la correction de programmes, que pour vérifier des résultats mathématiques contemporains. Le cours est basé sur le logiciel Coq, et sur les bibliothèques Ssreflect/Mathematical Components. Après un bref aperçu des différents composants d’un tel assistant de preuve, et en particulier de ses fondations logiques, on donnera quelques illustrations concrètes des techniques d’automatisation qui sont au centre de l’activité de formalisation.

  Sans que cela soit indispensable, disposer d’un ordinateur connecté à internet permettra de jouer en direct et dans un navigateur les démos sur lesquelles le cours sera basé. Aucune installation préalable de Coq n’est nécessaire.

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.

Arthur Charguéraud
Vérification de Programme avec la Logique de Séparation dans Coq

• CFML est un outil permettant de prouver la correction fonctionnelle et la complexité asymptotique de programmes OCaml. CFML s’intègre dans l’assistant de preuve Coq, en s’appuyant sur la logique de séparation, et sur une technique dite de formules caractéristiques. Dans ce cours, je présenterai d’abord les bases de la logique de séparation. Je montrerai ensuite comment spécifier et vérifier des structures de données (par exemple Vector, Hashtbl) et des algorithmes (par exemple DFS, Union-Find). Je vous proposerai alors des petits exercices de preuves à réaliser vous même. Enfin, j’expliquerai dans les grandes lignes la manière dont CFML 2.0 construit les formules caractéristiques sur lesquels l’outil s’appuie.