2024
Introduction au λ-calcul quantique
Kostia Chardonnet (Loria Nancy)
April 18, 2024
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
Armaël Gueneau (INRIA Saclay)
March 18, 2024
In recent years, there has been tremendous progress on developing program logics for verifying the correctness of programs in a rich and diverse array of languages. Thus far, however, such logics have assumed that programs are written entirely in a single programming language. In practice, this assumption rarely holds since programs are often composed of components written in different programming languages, which interact with one another via some kind of foreign function interface (FFI). In this talk, I will present our first steps towards the goal of developing program logics for multi-language verification. Specifically, I will present Melocoton, a multi-language program verification system for reasoning about OCaml, C, and their interactions through the OCaml FFI. Melocoton consists of the first formal semantics of (a large subset of) the OCaml FFI—previously only described in prose in the OCaml manual—as well as the first program logic to reason about the interactions of program components written in OCaml and C. Melocoton is fully mechanized in Coq on top of the Iris separation logic framework.
2023
Journée SeSTeRce
On denotations of circular and non-wellfounded proofs
Farzad Jafarrahmani (LIP6)
September 12, 2023
This talk investigates the question of denotational invariants of non-well-founded and circular proofs of the linear logic with least and greatest fixed-points. Indeed, while non-wellfounded and circular proof theory made significant progress in the last twenty years, the corresponding denotational semantics is still underdeveloped. We will talk about a denotational semantics for non-wellfounded proofs, based on a notion of totality. Several properties of the semantics will be then discussed: its soundness, the relation between totality and validity and the semantical content of the translation from finitary proofs to circular proofs. Finally, the talk focuses on circular proofs, trying to benefit from their regularity in order to define inductively the interpretation function. It is argued why the usual validity condition is too general for that purpose, while a fragment of circular proofs, strongly valid proofs, constitutes a well-behaved class for such an inductive interpretation. This presentation is based on joint work with Thomas Ehrhard and Alexis Saurin.
Journée SeSTeRce
On the geometry of validity criterion for non-wellfounded proofs
Esaïe Bauer (Irif)
September 12, 2023
This talk, introduces extensions of Baelde et al’s bouncing-validity criterion of $\mu MALL_\infty$, a non-wellfounded proof system extending linear logic with least and greatest fixed-points. Non-wellfounded proof systems, rely on a “validity criterion” to distinguish proofs from mere “pre-proofs”. The basic idea is a thread-based validity which require every infinite branch to be supported by a thread, that is a sequence of formulas occurring in the branch. This thread should witness the infinite unfolding of an inductive hypothesis or of a coinductive conclusion; computationally, this corresponds to asking that an inductive input-data is consumed infinitely often or that a coinductive output-data is infinitely produced.
The first “validity criterion” has been framed in terms of “valid straight-threads,” where the sequence of formulas are completely contained in the branch. In 2022, Baelde et al. proposed a novel criterion: the “bouncing validity criterion”, accommodating a wider range of proofs by allowing threads to get in and out of branches by “bouncing on axiom and cut rules. Nevertheless, certain proofs still eluded this criterion. To address this, we propose two additional validity criteria that satisfy cut-elimination property.
These new bouncing criteria relax the requirement that the “visible part” of a validating thread must be entirely contained within the branch. Instead, they only necessitate that the visible part intersects the branch infinitely often. During the presentation, we will provide an intuitive understanding of why these criteria preserve the cut-elimination property while highlighting their limitations concerning the focalization property.
This is a joint work with Alexis Saurin.
Journée SeSTeRce
Formalization of an FRP language with references
Jordan Ischard (LIFO, Université d’Orléans)
September 12, 2023
Functional reactive programming (FRP) has been introduced by Elliott with FRAN in 1997. FRP is a concept aiming to describe interactive programming languages with a high level syntax, based on functional methods. Interest in FRP has been growing since then with many proposals. In most cases, language properties are established with handmade proofs and not with proof assistants, which can lead to the omission of important steps that appear to be crucial with respect to the language features. As part of my thesis, we have chosen to formally prove the properties of language Wormholes using the proof assistant Coq. During this presentation, we will briefly introduce the main concepts, then we will talk about the specificity of the language and finally we will discuss the difficulties encountered during the formalization still in progress.
Journée SeSTeRce
Vérification formelle d’un compilateur pour un langage synchrone à flots de données avec machines à états
Basile Pesin (ENS, Inria)
September 12, 2023
Le projet Vélus est une formalisation d’un sous-ensemble du langage Scade dans l’assistant de preuves Coq. Il propose une formalisation de la sémantique dynamique du langage sous forme de relations entre flots infinis d’entrées et de sorties. Il inclut aussi un compilateur qui utilise CompCert, un compilateur vérifié pour C, pour produire du code assembleur. Enfin, il fournit une preuve de bout en bout que ce compilateur préserve la sémantique à flots de données des programmes sources. Mon travail de thèse étends Vélus avec des blocs de contrôles inspirés de Scade 6 et Lucid Synchrone, qui permettent la définition de comportement modaux: blocs switch, variables partagées (last x), blocs de réinitialisation, et machines à états hiérarchiques.
Dans cette présentation, on montrera le nouveau modèle sémantique développé pour intégrer ces blocs dans la sémantique à flots de données de Vélus. On discutera des propriétés dynamiques de ce modèle, que nous avons pu prouver en utilisant une analyse de dépendance vérifiée et un schéma d’induction spécifique aux programmes ne contenant pas de cycle de dépendance. On présentera aussi la compilation de ces constructions, en montrant les adaptations nécessaires aux schémas de compilation source à source standard, et les invariants permettant de prouver la correction de ces schémas. Enfin, on expliquera pourquoi l’arrière du compilateur doit également être modifié pour compiler ces constructions efficacement.
Journée SeSTeRce
Mécanisation d’une sémantique dénotationnelle dans un compilateur Lustre vérifié
Paul Jeanmaire (ENS, Inria)
September 12, 2023
Dans cette présentation, je décrirai comment on implémente dans Coq une sémantique dénotationnelle du langage Lustre et comment on prouve son équivalence avec le modèle relationnel existant dans le compilateur. Cette approche, constructive, permet de résoudre le problème d’existence d’une sémantique et facilite la preuve de certaines propriétés du langage.
Une caractérisation impérative des algorithmes (multi-)BSP
Frédéric Gava, Université Paris-Est Créteil
July 5, 2023
Après un bref rappel du modèles BSP et de sa version hiérarchique qu’est Multi-BSP, nous tenterons de répondre (formellement) à une question d’apparence naïve : qu’est-ce qu’un algorithme (multi-)BSP ? Pour ce faire, nous étendrons à BSP la définition axiomatique des algorithmes séquentiels de Gurevich, Celle-ci se base sur les algèbres évolutives aussi appelées ASMs. Avec ces nouveaux postulats, nous obtenons alors la classe des algorithmes BSP. Puis nous donnerons une équivalence algorithmique entre les algorithmes BSP et un mini langage impératif prouvant que les langages de programmation BSP usuels sont algorithmiquement complet. Nous serons alors à même de définir ce qu’est un algorithme Multi-BSP et sa caractérisation impérative. Nous terminerons par une discussion sur les limites de cette caractérisation impérative et du modèle Multi-BSP. N.B. : Aucune connaissance préalable sur les ASMs n’est nécessaire pour suivre cet exposé.
Pratique professionnelle de git
Julien Tesson, Nomadic Labs
June 9, 2023
Gestion d’un code source de grande taille avec git : l’exemple de Tezos.
Formalisation pour la sécurisation d’applications critiques
Thierry Lecomte, Clearsy
May 17, 2023
Le développement d’applications sûres et sécuritaires requiert une large palette de techniques pour leur développement logiciel et matériel, ainsi que pour leur vérification/validation. L’exposé présente une solution technologique (https://www.clearsy.com/outils/clearsy-safety-platform/) combinant un certain nombre de techniques, formelles ou non, comme:
- la redondance matérielle et applicative,
- la preuve de modèles formels,
- la génération de code et la compilation diversifiée,
- le passage dans un état puits restrictif en cas d’anomalie de fonctionnement.
L’approche permet de prendre en compte les défaillances aléatoires et systématiques (norme EN5012{6, 8, 9}) dans un cadre sûr (préservation de la vie humaine) et doit être étendu pour garantir la sécurité (préservation des secrets) dans un cadre sécuritaire (normes CC, IEC62433).
L’exposé fait le point sur le cadre d’application (incluant les spécifications système), le retour d’expérience, les travaux de recherche et développement en cours ainsi les problèmes scientifiques et techniques ouverts. Les thématiques couvertes incluent, à des degrés divers: la modélisation formelle, la génération de code et la compilation, la preuve mathématique, le deep-learning et la cybersécurité, le tout sous le prisme de la certification normative.
Analyse de boucle par quantification sur les itérations
Simon Robillard, Université de Montpellier
April 18, 2023
Cette présentation décrit un cadre théorique pour analyser et vérifier des programmes contenant des boucles. Cette technique est basée sur un language de premier ordre et utilise des “expressions étendues” qui permettent de décrire à la fois les propriétés fonctionnelles et les propriétés temporelles des boucles. Elle permet, en conjonction avec des prouveurs automatiques de théorèmes existants, d’automatiser des tâches telles que la vérification de la correction partielle, la vérification de la terminaison, et la génération d’invariants pour les boucles.
KEYNOTE: Déduction automatique
Simon Robillard, Université de Montpellier
April 17, 2023
Les systèmes informatiques occupent un rôle toujours croissant dans nos sociétés, et les défauts dans la conception ou l’implémentation de ces systèmes peuvent avoir des conséquences coûteuses. L’abstraction mathématique peut être utilisée pour obtenir des garanties fortes sur ces systèmes. Ces techniques, regroupées sous le terme de méthodes formelles, sont largement comprises et encouragées depuis plus de 50 ans, mais jusqu’à récemment, la complexité des systèmes à vérifier a empêché leur application à grande échelle. Aujourd’hui, les techniques de déduction automatique fournissent une réponse de plus en plus efficace à ce défi. Des outils ciblant diverses logiques peuvent être utilisés pour raisonner au sujet de problèmes mathématiques. Les problèmes issus de la vérification logicielle et matérielle sont, par leur nature, particulièrement adaptés au raisonnement automatique. Dans cette présentation, je donnerai un aperçu des différents outils de déduction automatique, et leur application à des problèmes de vérification.
Une approche sous-structurelle des déformations temporelles
Adrien Guatto, Université Paris Cité, IRIF
April 12, 2023
Travail mené en collaboration avec Christine Tasson et Ada Vienot. La programmation fonctionnelle réactive traite de structures de données infinies parcourues à un rythme fixé. Ce rythme doit être identique pour tous les producteurs et tous les consommateurs d’une même structure. Dans cet exposé, je présenterai un langage théorique dont les types décrivent ces rythmes de parcours, et dont la gestion sous-structurelle des contextes assure l’accord des producteurs et des consommateurs.
KEYNOTE: Frama-C, une plateforme open-source d’analyses de programmes C
Julien Signoles, CEA
February 13, 2023
Cet exposé présentera Frama-C, une plateforme open-source dédiée à l’analyse de programmes écrits en langage C. Après un aperçu général de la plateforme, nous introduirons ses principaux greffons d’analyse. Ainsi, nous expliquerons d’abord comment prouver l’absence de comportements indéfinis (ou les détecter s’il y en a) à l’aide d’Eva, le greffon d’analyse de valeurs par interprétation abstraite, nous introduirons ensuite comment prouver des propriétés fonctionnelles à l’aide du greffon WP dédié à la vérification déductive, puis nous présenterons comment détecter des erreurs avancées en cours d’exécution d’un programme, à l’aide d’E-ACSL, le greffon dédié à la vérification à l’exécution. Enfin, nous montrerons quelques usages plus avancés combinant différentes analyses. Les différentes techniques présentées seront illustrées à travers différents exemples réels provenant de domaines applicatifs variés (nucléaire, avionique, carte à puce, …).
Contribution to the Analysis of the Design-Space of a Distributed Transformation Engine
Jolan Philippe, IMT Atlantique
January 23, 2023
The design space for defining a distributed model transformation engine is a large spectrum of possibilities and opportunities to enhance performances in terms of computation time and memory consumption. Depending on the adopted decisions, the use of a transformation engine can be completely different (e.g., an incremental solution for an often-modified model vs a formally specified engine for reasoning, not performing). Already existing solutions propose engines with different goals based on several approaches including distribution, laziness, incrementality, and correctness. However, comparing the solutions is not trivial, and does not necessarily make sense. That is why we have implemented a new engine, integrating variability, that allows an analysis of its design space. From a language that has formal specifications, we created SparkTE, a parametrizable and distributed transformation engine on top of Spark. In this thesis, we aim at analysing the impact of the choices at different levels: the used programming models for defining expressions; the different semantics used to define the computation of a transformation; and the impact of engineering choices.
2022
Retour sur deux expériences de mobilité
Guillaume Cleuziou (LIFO, Université d’Orléans & Université de la Nouvelle-Calédonie)
Frédéric Loulergue (LIFO, Université d’Orléans & Northern Arizona University)
April 25, 2022
Dans cet exposé nous vous présenterons comment préparer une mobilité hors de métropole et l’expérience de ces mobilités à l’Université de Nouvelle Calédonie, et à la Northern Arizona University.
Data Analysis Algorithms: Modern Challenges and Solutions using Grapics Processing Units
Benoit Gallet, Northern Arizona University
January 17, 2022
With years, data analysis algorithms faced a constantly increasing amount of data to process and, consequently, an increasing computing time. Concurrently, many solutions have been developed to alleviate the issue of computation time, whether by reducing the complexity of the algorithm, the size of the data, or by parallelizing the computation when possible. The recent introduction of Graphics Processing Units (GPUs) into the High-Performance Computing field, greatly helped reduce the computation time of several data analysis algorithms, including the similarity join, k-NN, or k-means algorithms. And, as the GPU architectures rapidly evolve, new solutions become available to further improve the performance of said algorithms. In this presentation, we will take a look at these challenges related to such algorithms and architecture, as well as some of the possible solutions that have been or that could be developed to palliate these challenges.
2021
Améliorer un lecteur d’écran
Pierre Réty, LIFO, Université d’Orléans
November 22, 2021
Un lecteur d’écran est un logiciel qui permet de naviguer et d’agir sur les éléments graphiques sans regarder l’écran, et restitue les textes sous forme audio ou braille. Il permet ainsi aux personnes en difficulté de lecture (mal-voyants, analphabètes, dyslexiques) d’utiliser l’ordinateur ou le smartphone. Un lecteur d’écran appelé VoiceOver est disponible en natif et gratuitement sur les produits Apple. Mais il présente des anomalies et des limitations. Nous cherchons ici à corriger les principaux défauts de VoiceOver, ce qu’Apple ne fait pas, en relevant plusieurs défis. Comment améliorer : – un logiciel à sources fermées ? – la synthèse vocale ? – la navigation ? Nous apportons des réponses à ces questions, ainsi qu’une implémentation. Une démonstration sera effectuée.
Specification and Verification of High-Level Properties with MetAcsl
Nikolai Kosmatov, Thales Research & Technology (TRT)
March 15, 2021
Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its contract. However, function contracts do not provide a global view of which high-level (e.g. security-related) properties of a whole software module are actually established, making it very difficult to assess them. To address this issue, we propose a new specification mechanism, called meta-properties. A meta-property can be seen as an enhanced global invariant specified for a set of functions, and capable to express predicates on values of variables, as well as memory related conditions (such as separation) and read or write access constraints. We also propose an automatic transformation technique translating meta-properties into usual contracts and assertions, that can be proved by traditional deductive verification tools. This technique has been implemented as a Frama-C plugin called MetAcsl and successfully applied to specify and prove safety- and security-related meta-properties in several case studies. This talk gives an overview of various contributions related to MetAcsl. The corresponding results were published at TACAS 2019, TAP 2019 and FormaliSE 2021 (to appear). This work is a joint work with Virgile Robles, Virgile Prevosto, Louis Rilling, and Pascale Le Gall.
Online Testing of Dynamic Reconfigurations w.r.t. Adaptation Policies Frédéric Dadeau & Olga Kouchnarenko, Univ. Bourgogne Franche-Comté, CNRS, FEMTO-ST Institute
March 8, 2021
Component systems are designed as sets of components that may reconfigure themselves according to adaptation policies. Adaptation policies are seen as artifacts that describe desirable behavior of the system without enforcing a specific one. An adaptation policy is designed as a set of rules that indicate, for a given set of configurations, which reconfiguration operations can be triggered, with fuzzy values representing their respective utility. The adaptation policy has to be faithfully implemented by the system, especially w.r.t. the priority occurring in the rules, which are generally specified for optimizing some extra-functional properties (e.g. minimizing resource consumption).
In this context, this presentation will present a model-based testing approach which aims to generate large test suites in order to measure the occurrences of reconfigurations and compare them to their utility values specified in the adaptation rules. This process is based on a usage model of the system used to stimulate the system and provoke reconfigurations. As the system may reconfigure dynamically, this online test generator observes the system responses and evolution in order to decide the next appropriate test step to perform. In the end, the relative frequencies of the reconfigurations are measured in order to determine if the adaptation policy is faithfully implemented. We will illustrate our approach by simulations for a platoon of autonomous vehicles.
Joint work by Frédéric Dadeau, Jean-Philippe Gros and Olga Kouchnarenko
Systèmes auto-adaptatifs: introduction et modélisation formelle par des systèmes de réécriture de graphe
Cédric Eichler, INSA Centre Val de Loire, LIFO
February 15, 2021
Les systèmes distribués modernes évoluent dans des contextes soumis à évolutions auxquelles ils doivent s’adapter. Ils doivent ainsi faire face à l’arrivée ou au départ de composants, aux pannes, aux évolutions des besoins… L’informatique autonome fournit un cadre pour la délégation de la gestion de ces (auto-)adaptations au système lui-même, limitant ou éliminant les interventions humaines. Ce séminaire introductif présentera dans un premier temps l’informatique autonome, son inception, ses objectifs, sa mise en œuvre au travers de la boucle de contrôle MAPE-K, ainsi que quelques unes des problématiques qui lui sont associées. Dans un second temps, nous présenterons une approche de modélisation formelle de systèmes auto-adaptatifs basée sur la réécriture de graphe. Cette approche permet de représenter l’état d’un système, ses états acceptables et ses adaptations. Finalement, nous verrons comment cette approche permet de spécifier des adaptations préservant nécessairement la correction d’un système.
A calculus of Branching Processes
Jean Krivine, IRIF (joint work with Thomas Ehrhard (CNRS, IRIF) and Ying Jiang (ISCAS, China)
February 8, 2021
CCS-like calculi can be viewed as an extension of classical automata with communication primitives. In this talk I will show what we obtained when we applied this principle to tree-automata: a calculus of branching processes (termed CBP), where the continuations of communications are allowed to branch according to the arity of the communication channel. I will show that CBP can be “implemented” by a fully compositional LTS semantics. I will argue that CBP offers an interesting tradeoff between calculi with a fixed communication topology à la CCS and calculi with dynamic connectivity such as the π-calculus.
Categorifying Non-Idempotent Intersection Types
Federico Olimpieri, LIPN
February 1, 2021
Non-idempotent intersection types can be seen as a syntactic presentation of a well-known denotational semantics for the lambda-calculus, the category of sets and relations. Building on previous work, we present a categorification of this line of thought in the framework of the bang calculus, an untyped version of Levy’s call-by-push-value. We define a bicategorical model for the bang calculus, whose syntactic counterpart is a suitable category of types. In the framework of distributors, we introduce intersection type distributors, a bicategorical proof relevant refinement of relational semantics. Finally, we prove that intersection type distributors characterize normalization at depth 0.
Toward Safe and Efficient Reconfiguration with Concerto
Simon Robillard et Hélène Coullon, IMT Atlantique
January 18, 2021
For large-scale distributed systems that need to adapt to a changing environment, conducting a reconfiguration is a challenging task. In particular, efficient reconfigurations require the coordination of multiple tasks with complex dependencies. We present Concerto, a model used to manage the lifecycle of software components and coordinate their reconfiguration operations. Concerto promotes efficiency with a fine-grained representation of dependencies and parallel execution of reconfiguration actions, both within components and between them. In this paper, the elements of the model are described as well as their formal semantics. In addition, we outline a performance model that can be used to estimate the time required by reconfigurations, and we describe an implementation of the model. The evaluation demonstrates the accuracy of the performance estimations, and illustrates the performance gains provided by the execution model of Concerto compared to state-of-the-art systems. Keywords: reconfiguration, component-based models, coordination, parallelism, distributed software