Author: lmvadm

[March 2024] Armaël Gueneau’s talk

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
Armaël Gueneau (INRIA Saclay)
SR1, March 18, 2024, 14:00
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.

[September 2023] First SeSTeRce Day

First meeting of the SeSTeRce project, lead by Jules Chouquet.

10h00 — 10h30 : Accueil-café 

10h30 — 11h15 : Farzad Jafarrahmani (LIP6) On denotations of circular and non-wellfounded proofs 

    This talk investigates the question of denotational invariants of non-wellfounded 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. 

11h15 — 12h00 : Esaïe Bauer [À venir] 

12h00 — 12h30 : Questions/discussions/retards 

12h30 — 13h30 : Pause repas 

13h30 — 14h15 : Jordan Ischard (LIFO) Formalization of an FRP language with references 

    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. 

14h15 — 15h00 : Basile Pesin (ENS,Inria) Vérification formelle d’un compilateur pour un langage synchrone à flots de données avec machines à états 

    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. 

15h00 — 15h15 : Pause café 

15h15 — 16h00 : Paul Jeanmaire (ENS,Inria) Mécanisation d’une sémantique dénotationnelle dans un compilateur Lustre vérifié. 

    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.