École Jeunes Chercheuses et Jeunes Chercheurs en Programmation (EJCP)

L'école du GDR GPL.

Main EJCP2022 EJCP2021 About Contact

EJCP - version 2021, du 14 au 18 juin 2021

L’école a eu lieu en mode “dégradé”, en distanciel, pendant la semaine des journées du GDR GPL.

Titre : 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.

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.

Lien vers WHY3 demo

abstract: 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
capture 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: Virgile Prevosto is a researcher, expert in static 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 25 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 static analysis and Frama-C since more than 10 years at ENSIIE.

slides, et exemples de la démo

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).

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. 

Comité d’organisation

Laure Gonnord, Sébastien Mosser, Hélène Coullon.

Pour plus d’information concernant l’EJCP21, vous pouvez écrire à laure.gonnord@ens-lyon.fr. !