Programme
Lundi 4 juillet 2022
- Deductive Program Verification with Why3
- Résumé: 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.
- Bio: Andrei Paskevich is associate professor at Paris-Saclay university and a member of the LMF laboratory. His research activities are in the field of formal methods, in particular, in deductive program verification. Together with his colleagues from Inria, CNRS, and CEA, he develops the Why3 platform since 2010.
Mardi 5 juillet 2022
- How can Domain-specific Modelling Languages (DSML) help us formalize customer requirements?
- Résumé: The use of formal verification methods ensures that the program conforms to the defined behavior. However, the definition of this behavior is a complex problem, requiring an understanding of both the business domain and the technical realities of the project management. Also, there is often a gap between the definition of the behavior from a business point of view and the more formal definition of verification methods. To facilitate the adoption of formal methods, language engineering and model engineering propose to make available models, based on formal semantic definitions. These models are linked to dedicated languages, and consequently more accessible and interoperable with existing models used by different stakeholders. In this talk, I will present how the definition of a Domain Specific Modeling Language and its formal semantics can bridge the gap between the expression of a customer requirement and the correction of the code that must satisfy this requirement.
- Bio: Florian Galinier did his PhD in the SM@RT team at IRIT (University of Toulouse). He is co-founder and CEO of the start-up SPILEn, in which he participates to the implementation of traceability and requirements formalization tools for the software industry. His research interests range from requirements engineering to model engineering, with a strong focus on industrial applications.
Mercredi 6 juillet 2022
- Abstract Interpretation with Frama-C
- Résumé: Abstract interpretation has been proposed as a systematic way to build program analyzers that are always terminating (even if the underlying program has infinite loops) and correct, in the sense that the analysis captures all possible concrete behaviors of the program. It is at the core of many analysis tools. In this talk, we will present the main features of abstract interpretation and illustrate them with the Eva plug-in of Frama-C, which uses abstract interpretation techniques to verify the absence of runtime errors in C programs.
- Bio: Julien Signoles is a senior researcher, expert in code analysis and formal methods at Université Paris-Saclay, CEA, List, where he works since 2006 in the Software Safety and Security Lab (LSL). He has been one of the main developers of the Frama-C platform nearly since its inception and co-authored around 50 peer-reviewed papers on Frama-C related topics. He gave tutorials and training sessions on Frama-C in various academic and industrial venues and teaches code analysis techniques (in particular, abstract interpretation, deductive verification) since more than 12 years.
Jeudi 7 juillet 2022
- Introduction à la programmation par contraintes
- Résumé: 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 je montrerai les liens entre la programmation par contraintes, et l’interprétation abstraite.
- Bio: Charlotte Truchet est maître de conférence en informatique à l’Université de Nantes, dans l’équipe TASC du LS2N. Son thème de recherche principal est la programmation par contraintes, avec des applications en informatique musicale (composition assistée par ordinateur), urbanisme (villes durables) et plus récemment chimie (optimisation de réactions en flux). Côté contraintes, elle travaille sur les contraintes globales, la parallélisation des algorithmes d’optimisation combinatoire, les liens entre contraintes et sémantique (interprétation abstraite), l’analyse en moyenne d’algorithmes de contraintes.
Vendredi 8 juillet 2022
- Vérification de Programme avec CFML
- Résumé: 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 la technique des formules caractéristiques. Je présenterai les bases de la logique de séparation et de CFML, en présentant les deux premiers chapitres du cours Separation Logic Foundations, volume 6 de Software Foundations. Je vous proposerai au cours de la session des petits exercices pour vous familiariser avec le fonctionnement de CFML.
- Bio: Arthur Charguéraud is a researcher at Inria, first at Inria Saclay, then in the CAMUS team in Strabourg. His research interests span from formal verification and mechanized semantics to multicore programming. In particular, he is the main developer of the CFML tool, which has been put to practice to verify both the functional correctness and the amortized asymptotic complexity of nontrivial imperative programs such as the Union-Find data structure and a state-of-the-art incremental cycle detection algorithm. Besides, Arthur Charguéraud is vice-president of the nonprofit organization France-ioi, and co-organizer of the Bebras contest (concours Castor Informatique).
|
