Planning prévisionnel

  • lundi 26
    • après-midi : Verification of security protocols: from confidentiality to privacy (Stéphanie Delaune)
  • mardi 27
    • matin : Introduction to Type Theory & Interactive Theorem Proving in Coq (Matthieu Sozeau)
    • après-midi : Domain-specific Languages: Why, and How-to (Sébastien Mosser)
  • mercredi 28
    • matin : Model Checking Modulo Theories with Cubicle (Sylvain Conchon)
    • après-midi : Model-Based Testing in Practice (Frédéric Dadeau)
  • jeudi 29
    • matin : Research in Compilers and Introduction to Loop Transformations (Tomofumi Yuki)
    • après-midi (13 h 30 - 16 h): Programmation et vérification avec Eiffel, AutoProof, AutoTest et SCOOP (Bertrand Meyer)
    • social events : visite de l'usine Airbus et repas de gala
  • vendredi 30
    • matin : Deductive Program Verification with Why3 (Andrei Paskevich)

Contenu détaillé

  • Sylvain Conchon
    • Model Checking Modulo Theories with Cubicle
    • This lecture is an introduction to Model Checking Modulo Theories (MCMT), an new model checking technique invented by Silvio Ghilardi and Silvio Ranise. This technique is based on the integration of SMT solving and backward reachability. We will illustrate the concepts of MCMT with Cubicle, an open source model checker for verifying safety properties of array-based systems, a syntactically restricted class of parametrized transition systems with states represented as arrays indexed by an arbitrary number of processes.
  • Frédéric Dadeau
    • Model-Based Testing in Practice
    • Dans une première partie, ce cours a pour objectif de présenter les grands principes du test à partir de modèles (Model-Based Testing - MBT). Nous ferons un tour d'horizon de différentes approches, en suivant la classification proposée par Utting, Pretschner et Legeard en 2011 et réactualisée en 2015. Dans une seconde partie, nous nous intéresserons à deux approches MBT que nous appliquerons sur un exemple jouet. La première utilise un outil didactique de test à partir de machines à états finies, nommé ModelJUnit. La seconde est un outil industriel, l'environnement de test Smartesting CertifyIt, qui permet de générer automatiquement des tests à partir d'un modèle UML agrémenté de contraintes OCL suivant divers critères de sélection de test (structurels, scénarios, propriétés temporelles). Ces deux outils seront mis en oeuvre sur une application web de simulateur de distributeur automatique de billets illustrant les problématiques à considérer lors de l'application des approches MBT dans la pratique.
  • 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.
  • Bertrand Meyer
    • Programmation et vérification avec Eiffel, AutoProof, AutoTest et SCOOP
  • Sébastien Mosser
    • Domain-specific Languages: Why, and How-to
    • Domain-specific languages (DSLs) advocate the definition of dedicated languages for given users. This class of language differs from classical programming language (GPLs), as their audience is restricted and their lifespan is often short. This course will discuss the difference between DSLs and GPLs, and give you the keys to create your very-own language dedicated to a given domain in a couple of hours. We will apply theses concepts through the definition of ArduinoML, a language dedicated to the construction of little apps to be executed on top of Arduino micro-controlers.
  • 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.
  • Matthieu Sozeau
    • Introduction to Type Theory & Interactive Theorem Proving in Coq
    • This lecture will be an introduction to Type Theory as used for interactive theorem proving in the Coq system. Coq is a general purpose theorem prover that can be used to formalize mathematical proofs and programs, and model all kinds of systems. It is based on a purely functional programming language (without effects such as references or non-termination) and a rich logic, linked through the so-called Curry-Howard isomorphism. 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.
  • Tomofumi Yuki
    • Research in Compilers and Introduction to Loop Transformations
    • The main goal of this course is to give some ideas about what research in compiler is about. One of the main challenges in compilers is in analyzing a program to find what to do with it to bring higher performance. In many cases, what should be done is obvious to an expert programmer. However, automating the decision process and the transformations themselves is a whole different story. Even the word "performance" is context sensitive, and can mean speed, code size, energy efficiency, and other metrics.
      This course aims to illustrate these challenges and some techniques to addresses the difficulties. The main subject is parallelism and data locality; traditionally important properties of programs, now getting more and more important.