• Lundi 24 juin
  • Fin de matinée (11h-12h) : Accueil dans le hall de l'UFR de Mathématiques-Informatique.
  • Après-midi (14h-17h30) : Coccinelle: Practical program transformation for the Linux kernel (Julia Lawall)
  • Evènement (18h00-19h00) : Ma thèse en 60 secondes
• Mardi 25 juin
  • Matin (9h-12h30) : Program Verification using Why3 (Andrei Paskevich)
  • Après-midi (14h-17h30) : Étude empirique en génie logiciel – Application sur GitHub et Alexa (Xavier Blanc)
• Mercredi 26 juin
  • Matin (9h-12h30) : Interprétation abstraite et propriétés de programmes C (Julien Signoles)
  • Après-midi (13h45-17h15) : Introduction à la programmation par contraintes (Charlotte Truchet)
  • Évènement (17h30-19h) : Visite du musée de sismologie
• Jeudi 27 juin
  • Matin (9h-12h30) : Introduction à Coq (Julien Narboux)
  • Après-midi (14h-17h30) : Software Variability and Artificial Intelligence (Mathieu Acher)
  • Évènement (20h-23h) : Cocktail dinatoire à l'Art'Café (Musée d'Art Moderne de Strasbourg)
• Vendredi 28 juin
  • Matin (9h-12h30) : Program Verification using CFML 2.0 (Arthur Charguéraud)

• 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
• lien vers les transparents et les exercices

• 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.
• Lien vers les transparents : ap.pdf
• Why3 dans un navigateur, pour les exercices : http://why3.lri.fr/ejcp-2019/

• 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.
• Lien vers les transparents : xb.pptx

• 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.
• Lien vers les transparents : js.pdf,

• 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.
• Logiciel requis :
  • Il est recommandé aux participants d'installer le solveur de contraintes AbSolute, via opam:

  opam repo add absolute https://raw.githubusercontent.com/mpelleau/AbSolute/master
  opam install absolute
  

  • guide d'installation complet : https://github.com/mpelleau/AbSolute
• transparents
• Solution au problème des cercles d'Apollonius

• Un assistant de preuve est un logiciel permettant l'écriture et la vérification de démonstrations mathématiques. Ces démonstrations peuvent concerner aussi bien des théorèmes mathématiques que des propriétés de correction des algorithmes. Ce cours sera une introduction à ce domaine et utilisera Coq pour les démonstrations. Dans une première partie, on évoquera les motivations pour utiliser les assistants de preuve, les langages permettant d'interagir avec eux et la correspondance de Curry-Howard. Dans la seconde partie, on montrera comment des algorithmes prouvés corrects peuvent eux-mêmes être utilisés pour construire d'autres preuves (preuve par réflexion).
• Lien vers les transparents : jn.pdf, jn_exemples_ejcp2019.v.

• 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.
• Lien vers les transparents : ma.pdf

• 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.
• Une installation de Coq 8.8 ou 8.9 est requise pour exécuter les exercices.

  git clone https://gitlab.inria.fr/charguer/cfml2_ejcp2019
  cd cfml2_ejcp2019/theories
  make -j2
  

  Pour ouvrir CoqIDE avec les bons fichiers :

  ./open.sh
  

  La commande ci-dessous est un raccourci pour :

  coqide -async-proofs off -async-proofs-command-error-resilience off \
   EJCPTuto.v EJCPExo.v EJCPImplem.v \
   ExampleStack.v ExampleList.v ExampleListOf.v ExamplePairingHeap.v
  

  Vous pouvez également utiliser ProofGeneral, en ouvrant ces mêmes fichiers.

Les cours auront lieu dans un amphi du bâtiment de l'UFR de Mathématique-Informatique.

L'entrée se fait par la porte sud du bâtiment, rue René Descartes.

Lien vers Open Street Map avec tous les lieux du campus Unistra.