Programme

• 14h00 - Verification of security protocols: from confidentiality to privacy par Stéphanie Delaune (le cours)

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.

• 9h00 - Short introductions to Type Theory and the Coq system by Yves Bertot  (slides)(la démo)

In a first part of the course, we give an overview of typed lambda-calculus and its use for safe programming and logical reasoning.  In a second part of the course, we illustrate this use of types by examples developed in the Coq system.

• 14h00 - Domain-specific Languages: Why, and How-to par Sébastien Mosser

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. 

• 9h00 - Research in Compilers and Introduction to Loop Transformations by Tomofumi Yuki (le cours)

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.

• 14h00 - Model Checking Modulo Theories with Cubicle by Sylvain Conchon (le cours)

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.

• 8h30 - Deductive Program Verification with Why3 by Andrei Paskevich

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.

• 13h00 - Model-Based Testing in Practice by Frédéric Dadeau (le cours)

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. Dans une seconde partie, nous nous intéresserons à l'approche MBT mise en pratique dans un outil industriel, l'environnement de test Smartesting CertifyIt. Cet outil permet de générer automatique des tests à partir d'un modèle UML agrémenté de contraintes OCL. Il permet aussi de piloter la génération de testspar des scénarios définis par l'utilisateur ou des propriétés temporelles.

• 9h00 Introduction to Empirical Software Engineering by Martin Monperrus

In this lecture, I will first study the epistemological foundations of science and engineering, then try to come with a working definition of empirical software engineering, and finally go through the main types of work in this field.

• Fin vers 14h00 après le repas