Semantics and Verification of RDMA Programs<\/strong> Formalised meta-theory for a certified proof assistant kernel Lunor: A Domain-Specific Language for Rapid Prototyping of Web Applications<\/strong> Introducing Separation Logic into ACSL<\/strong> Towards a formalization of divide-and-conquer parallel design pattern<\/strong> Frama-C\/Eva: a concrete application of abstract interpretation<\/strong> First Order Coalition Logic : Model Checking, Compl\u00e9tude et Satisfaisabilit\u00e9<\/strong> An algebraic approach for union bound reasoning about probabilistic programs<\/strong> Eclat : un langage synchrone pour la programmation s\u00fbre, expressive et efficace de circuits FPGA <\/strong> Mechanisation of computation for identity types in Martin-L\u00f6f type theory<\/strong> Program Comprehension of Domain-Specific and General-Purpose Languages: Results from Controlled Experiments<\/strong> Langage de sp\u00e9cification et outil de v\u00e9rification pour le consentement et la n\u00e9cessit\u00e9 des donn\u00e9es fond\u00e9s sur une classification relative au respect de la vie priv\u00e9e<\/strong> Introduction au \u03bb-calcul quantique Melocoton: <\/strong>A Program Logic for Verified Interoperability Between OCaml and C<\/strong> Journ\u00e9e SeSTeRce<\/strong> Journ\u00e9e SeSTeRce Journ\u00e9e SeSTeRce Journ\u00e9e SeSTeRce Journ\u00e9e SeSTeRce Une caract\u00e9risation imp\u00e9rative des algorithmes (multi-)BSP <\/strong> Pratique professionnelle de git<\/strong> Formalisation pour la s\u00e9curisation d’applications critiques <\/strong> L’approche permet de prendre en compte les d\u00e9faillances al\u00e9atoires et syst\u00e9matiques (norme EN5012{6, 8, 9}) dans un cadre s\u00fbr (pr\u00e9servation de la vie humaine) et doit \u00eatre \u00e9tendu pour garantir la s\u00e9curit\u00e9 (pr\u00e9servation des secrets) dans un cadre s\u00e9curitaire (normes CC, IEC62433). Analyse de boucle par quantification sur les it\u00e9rations<\/strong> KEYNOTE: D\u00e9duction automatique<\/strong> Une approche sous-structurelle des d\u00e9formations temporelles<\/strong> KEYNOTE: Frama-C, une plateforme open-source d’analyses de programmes C<\/strong> Contribution to the Analysis of the Design-Space of a Distributed Transformation Engine<\/strong> Retour sur deux exp\u00e9riences de mobilit\u00e9<\/strong> Data Analysis Algorithms: Modern Challenges and Solutions using Grapics Processing Units<\/strong> Am\u00e9liorer un lecteur d\u2019\u00e9cran<\/strong> Specification and Verification of High-Level Properties with MetAcsl<\/strong> Online Testing of Dynamic Reconfigurations w.r.t. Adaptation Policies<\/strong> Fr\u00e9d\u00e9ric Dadeau & Olga Kouchnarenko, Univ. Bourgogne Franche-Comt\u00e9, CNRS, FEMTO-ST Institute Syst\u00e8mes auto-adaptatifs: introduction et mod\u00e9lisation formelle par des syst\u00e8mes de r\u00e9\u00e9criture de graphe<\/strong> A calculus of Branching Processes<\/strong> Categorifying Non-Idempotent Intersection Types<\/strong> Toward Safe and Efficient Reconfiguration with Concerto<\/strong> 2026 Semantics and Verification of RDMA ProgramsGuillaume Ambal (Imperial College)March 27, 2026, 2PM, SR1Remote Direct Memory Access (RDMA) is a low-latency data-transfer technology used in high-performance computing and data centres. This talk will cover several recent formalisation results, ranging from the semantics of the technology to frameworks for verifying library implementations.2025 Formalised meta-theory for a … Continue reading “Seminar”<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":6,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-741","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/pages\/741","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/comments?post=741"}],"version-history":[{"count":26,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/pages\/741\/revisions"}],"predecessor-version":[{"id":1376,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/pages\/741\/revisions\/1376"}],"wp:attachment":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/media?parent=741"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}
Guillaume Ambal (Imperial College)
March 27, 2026, 2PM, SR1<\/em>
Remote Direct Memory Access (RDMA) is a low-latency data-transfer technology used in high-performance computing and data centres. This talk will cover several recent formalisation results, ranging from the semantics of the technology to frameworks for verifying library implementations.
2025<\/p>\n\n\n\n
<\/strong>Meven Lennon-Bertrand (Inria Saclay)
November 17, 2025
<\/em>Given the growing use of proof assistants, their kernels are a natural target for program certification: they are critical, yet small and well-specified. This goal is not new, but despite the maturity of type theory and software verification, we are yet to see a certified Agda, Coq or Lean. The core difficulty is that kernels rely on complex invariants, which in turn rest on significant properties of the type system. In essence, we cannot certify a kernel without first formalising the meta-theory of its type system, a difficult endeavour for a realistic language.
However, things have been recently changing, with multiple new projects in this space. In my talk, I will give an overview of this landscape, and present two complementary formalisation projects in that direction: MetaRocq, which aims at verifying a kernel for Rocq, in Rocq, and Logrel-Rocq, which concentrates more on the formalised meta-theory aspects.<\/p>\n\n\n\n
Toma\u017e Kosar (University of Maribor)
October 20, 2025<\/em>
In this talk, we will present a solution that enables the creation of web applications using a custom-built domain-specific language called Lunor. The solution consists of three key components: a parser, a language server, and a Visual Studio Code extension, which together form a comprehensive development environment. Lunor allows developers to describe the structure of web applications in a clear, human-readable syntax that includes Markdown for specifying component content. A Lunor program is automatically transformed into React code that can be directly integrated into any React-based web application. Lunor provides an effective approach for rapid prototyping and the development of simple web applications. The language’s modular architecture, based on the Language Server Protocol, ensures flexibility, extensibility, and precise control over code generation. While primarily designed for the early stages of development, Lunor-generated projects can be further expanded using standard React technologies, making it a valuable tool for accelerating the initial phases of web application design.<\/p>\n\n\n\n
Lo\u00efc Correnson (CEA List)
July 22, 2025
<\/em>Frama-C\/WP is a tool implementing deductive verification on C programs annotated by properties in the ACSL language. Both WP & ACSL rely on classical Hoare Program Logic, which is known to be intrinsically limited, especially for programs with complex structures using pointers. The modern approach to deal with such programs is to use Separation Logic instead, which is more powerful than Hoare Logic, but is more difficult to use in practice, and for which there is no support from main stream automated provers, typically SMT solvers like Z3, Alt-Ergo, CVC4 or CVC5. In this talk, I would present the directions we are investigating for introducing (some ingredients from) Separation Logic into ACSL and Frama-C\/WP.<\/p>\n\n\n\n
Virginia Niculescu (University Babe\u015f-Bolyai of Cluj-Napoca)
July 21, 2025<\/em>
Structuring is essential in parallel programming, as it helps manage the inherent complexity of concurrent computation. One effective way to achieve such structuring is through programming patterns and algorithmic skeletons. Among these, the divide-and-conquer pattern plays a fundamental role. It is defined by a recurrence relation that expresses the solution to a problem in terms of the solutions to smaller subproblems of the same nature. This pattern supports a wide range of computational scenarios, making it valuable to develop a general specification that captures all its possible forms and use cases. We aim to demonstrate that the divide-and-conquer pattern can be generalized in such a way that it subsumes many other parallel programming patterns. To support this claim, we propose a formal and comprehensive formulation of the divide-and-conquer paradigm. Such a generalization can serve not only theoretical purposes but also practical ones\u2014particularly in the design of parallel programming libraries and APIs that rely on divide-and-conquer-based skeletons.<\/p>\n\n\n\n
Andr\u00e9 Maroneze (CEA LIST)
July 16, 2025<\/em>
The C language is widely used for critical systems, despite its memory unsafety. The Frama-C platform provides static and dynamic code analyses, based on formal verification techniques, to provide guarantees for C code bases. Between testing and full program proof, the Eva analyzer allows automatic identification of several kinds of undefined behaviors. It can be seen as an “abstract debugger”, and help understand what the code does. With some experience, it can scale up to 100k’s lines of code. This presentation will focus on practical examples, some theoretical foundations, and ongoing challenges concerning the application of abstract interpretation to C code analysis.<\/p>\n\n\n\n
Davide Catta (LIPN, Paris 13)
June 25, 2025<\/em>
Les logiques pour le raisonnement strat\u00e9gique constituent une vaste famille d\u2019outils formels con\u00e7us pour mod\u00e9liser, v\u00e9rifier et analyser les capacit\u00e9s et les strat\u00e9gies (individuels ou collectifs) d\u2019agents autonomes, dans un environnement comp\u00e9titif.
Nous introduisons First Order Coalition Logic (FOCL), qui combine les intuitions de Coalition Logic (CL) et de Strategy Logic (SL). Plus pr\u00e9cis\u00e9ment, FOCL permet une quantification arbitraire sur les actions de groupes d\u2019agents.
Dans cet expos\u00e9, nous montrons que FOCL est strictement plus expressive que d\u2019autres logiques de coalition connues, puis nous discutons de sa proc\u00e9dure de model checking. Ensuite, nous fournissons une axiomatisation coh\u00e9rente et compl\u00e8te de cette logique, qui est, \u00e0 notre connaissance, la premi\u00e8re axiomatisation d\u2019une logique strat\u00e9gique dans la litt\u00e9rature. Enfin, nous montrons que le probl\u00e8me de la satisfaisabilit\u00e9 est ind\u00e9cidable.<\/p>\n\n\n\n
Leandro Gomes, Universit\u00e9 de Lille, CRIStAL
April 10, 2025<\/em>
Kleene Algebra with Tests (KAT) provides a framework for algebraic equational reasoning about imperative programs. The recent variant Guarded KAT (GKAT) allows to reason on non-probabilistic properties of probabilistic programs. Here we introduce an extension of this framework called approximate GKAT (aGKAT), which equips GKAT with a partially ordered monoid (real numbers) enabling to express satisfaction of (deterministic) properties except with a probability up to a certain bound. This allows to represent in equational reasoning \u201c\u00e0 la KAT\u201d proofs of probabilistic programs based on the union bound, a technique from basic probability theory. We show how a propositional variant of approximate Hoare Logic (aHL), a program logic for union bound, can be soundly encoded in our system aGKAT. We then illustrate the use of aGKAT with an example of accuracy analysis from the field of differential privacy.<\/p>\n\n\n\n
Lo\u00efc Sylvestre, Sorbonne Universit\u00e9, LIP6
January 27, 2025<\/em>
Cet expos\u00e9 portera sur la conception et l\u2019implantation d\u2019applications embarqu\u00e9es r\u00e9actives et de calcul intensif sur du mat\u00e9riel reconfigurable FPGA (Field Programmable Gate Array). Il pr\u00e9sentera Eclat : un langage de programmation parall\u00e8le g\u00e9n\u00e9raliste (inspir\u00e9 d\u2019OCaml) avec un s\u00e9mantique synchrone d\u00e9riv\u00e9e de l\u2019horloge physique du FPGA cible. Eclat permet de programmer (et composer) \u00e0 la fois des calculs orient\u00e9s flot de contr\u00f4le et des interactions orient\u00e9es flot de donn\u00e9es. Le mod\u00e8le de calcul propos\u00e9 est suffisamment pr\u00e9cis et expressif pour d\u00e9velopper des abstractions de programmation de haut niveau (telles que des squelettes algorithmiques et des machines virtuelles) avec des performances pr\u00e9dictibles. Cela vise \u00e0 r\u00e9pondre aux besoins d\u2019efficacit\u00e9 et aux contraintes de s\u00fbret\u00e9 des applications mat\u00e9rielles, notamment temps r\u00e9el. Eclat se veut accessible aux programmeuses et programmeurs de logiciel ; il est d’ailleurs utilis\u00e9 comme langage support dans un cours de compilation.<\/p>\n\n\n\n2024<\/h2>\n\n\n\n
Thibaut Benjamin (University of Cambridge)
November 25, 2024<\/em>
Martin-L\u00f6f type theory is a powerful theory that is at the foundation of modern proof assistants such as Coq, Lean, Agda. It provides a unifying framework to formalise mathematics and software. Although this framework is powerful enough to formalise and verify very complex software (like for instance the CompCert C compiler, formally verified in Coq), its practical use is constrained by the large proof effort it requires, rendering the adoption of such tools slower. Various techniques are considered to simplify and streamline the use of proof-assistants. For instance, identity types, that represent equalities have a very rich and complex structure, and it is common to ignore that structure by adding a principle called Uniqueness of Identity Proofs (UIP). This axiom states that any two identity proofs are equal thus enforcing in a way proof irrelevance for equality. Another example is the so-called univalent axiom (originally coming from a connection with homotopy theory) that for computer scientists mean that the formalisation can be done in a way that is independent of the choice of datatypes, as long as those datatypes encode the same information. This is not only a powerful reasoning principle that allows one to reason on simple but inefficient datatypes and transport the results to finicky but efficient ones, it also reflects the very common computer science practice of hiding the implementation of datatypes under an API to make the programs more modular. Unfortunately, UIP and the univalence axiom are incompatible. In this talk, I will present a workflow that I am designing to handle and automate complex computation on identity types, in an effort to reduce the need for UIP and render practical the use of the univalence axiom. I will in particular show the implementation of this workflow as a Coq plugin, that uses a secondary tool called CaTT, which is specifically designed to handle the algebraic structure of identity types, called higher groupoid.
<\/p>\n\n\n\n
Tomaz Kosar (Universit\u00e9 de Maribor, Slov\u00e9nie)
October 21,<\/em> 2024<\/em>
Domain-specific languages (DSLs) feature simpler notation than general-purpose languages (GPLs) because their syntax is tailored to a specific problem domain. As a result, the alignment between the language and the problem domain should enhance programmers’ efficiency and accuracy when using DSLs, compared to alternative solutions such as application libraries in GPLs. In a series of controlled experiments, we observed these differences and report on the findings.<\/p>\n\n\n\n
Myriam Clouet (Universit\u00e9 d’Orl\u00e9ans, LIFO)
July 18, 2024
<\/em>La vie priv\u00e9e est un droit fondamental que l\u2019on retrouve dans plusieurs lois dans le monde entier. Donc, v\u00e9rifier qu\u2019un syst\u00e8me respecte la vie priv\u00e9e est crucial. Cependant, la vie priv\u00e9e est une notion complexe. Assurer qu\u2019un syst\u00e8me respecte la vie priv\u00e9e n\u00e9cessite de v\u00e9rifier que les propri\u00e9t\u00e9s de vie priv\u00e9es sont respect\u00e9es durant tout le cycle de vie, ce qui complique le processus de v\u00e9rification. Une grande vari\u00e9t\u00e9 de solutions ont \u00e9t\u00e9 propos\u00e9es pour am\u00e9liorer le respect de la vie priv\u00e9e. Il est souvent difficile de pr\u00e9cis\u00e9ment identifier quand elles ciblent la m\u00eame probl\u00e9matique. Dans cette th\u00e8se, j\u2019adresse ces probl\u00e8mes en proposant une fa\u00e7on de classifier des articles concernant la vie priv\u00e9e et une approche pour v\u00e9rifier des propri\u00e9t\u00e9s de vie priv\u00e9e \u00e0 deux \u00e9tapes du cycle de vie. Je propose GePyR, une nouvelle repr\u00e9sentation de la vie priv\u00e9e, g\u00e9n\u00e9rique et sp\u00e9cialisable, et une ontologie instanstiable, PyCO, qui mod\u00e9lise les \u00e9l\u00e9ments cl\u00e9s de la vie priv\u00e9e et leurs relations. Cette classification est \u00e9valu\u00e9e sur la litt\u00e9rature, en r\u00e9alisant un Systematic Mapping Study. Dans cette th\u00e8se, je formalise \u00e9galement deux propri\u00e9t\u00e9s de vie priv\u00e9e, la conformit\u00e9 aux finalit\u00e9s consenties et la conformit\u00e9 \u00e0 la n\u00e9cessit\u00e9 des donn\u00e9es. Je propose une nouveau langage de sp\u00e9cification, CSpeL, qui permet de formaliser les \u00e9l\u00e9ments n\u00e9cessaires pour v\u00e9rifier ces propri\u00e9t\u00e9s, et introduis un nouvel outil, CASTT, pour v\u00e9rifier ces propri\u00e9t\u00e9s sur des traces d\u2019ex\u00e9cutions, sur un mod\u00e8le ou un programme. Cette approche est appliqu\u00e9e sur deux cas d\u2019utilisation \u00e0 deux niveaux d\u2019abstraction, pour \u00e9valuer sa correction, son efficacit\u00e9 et son utilit\u00e9. Travail r\u00e9alis\u00e9 \u00e0 l’U. Paris Saclay, CEA.<\/p>\n\n\n\n
<\/strong>Kostia Chardonnet (Loria Nancy)
April 18, 2024<\/em><\/p>\n\n\n\n
Arma\u00ebl Gueneau (INRIA Saclay)
March 18, 2024<\/em>
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\u2014previously only described in prose in the OCaml manual\u2014as 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.<\/p>\n\n\n\n2023<\/h2>\n\n\n\n
On denotations of circular and non-wellfounded proofs<\/strong>
Farzad Jafarrahmani (LIP6)
September 12, 2023<\/em>
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.<\/p>\n\n\n\n
On the geometry of validity criterion for non-wellfounded proofs<\/strong>
Esa\u00efe Bauer (Irif)
September 12, 2023<\/em>
<\/strong>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.<\/p>\n\n\n\n
Formalization of an FRP language with references<\/strong>
Jordan Ischard (LIFO, Universit\u00e9 d’Orl\u00e9ans)
September 12, 2023<\/em>
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.<\/p>\n\n\n\n
V\u00e9rification formelle d’un compilateur pour un langage synchrone \u00e0 flots de donn\u00e9es avec machines \u00e0 \u00e9tats<\/strong>
Basile Pesin (ENS, Inria)
September 12, 2023<\/em>
Le projet V\u00e9lus est une formalisation d’un sous-ensemble du langage Scade dans l’assistant de preuves Coq. Il propose une formalisation de la s\u00e9mantique dynamique du langage sous forme de relations entre flots infinis d’entr\u00e9es et de sorties. Il inclut aussi un compilateur qui utilise CompCert, un compilateur v\u00e9rifi\u00e9 pour C, pour produire du code assembleur. Enfin, il fournit une preuve de bout en bout que ce compilateur pr\u00e9serve la s\u00e9mantique \u00e0 flots de donn\u00e9es des programmes sources. Mon travail de th\u00e8se \u00e9tends V\u00e9lus avec des blocs de contr\u00f4les inspir\u00e9s de Scade 6 et Lucid Synchrone, qui permettent la d\u00e9finition de comportement modaux: blocs switch, variables partag\u00e9es (last x), blocs de r\u00e9initialisation, et machines \u00e0 \u00e9tats hi\u00e9rarchiques.
Dans cette pr\u00e9sentation, on montrera le nouveau mod\u00e8le s\u00e9mantique d\u00e9velopp\u00e9 pour int\u00e9grer ces blocs dans la s\u00e9mantique \u00e0 flots de donn\u00e9es de V\u00e9lus. On discutera des propri\u00e9t\u00e9s dynamiques de ce mod\u00e8le, que nous avons pu prouver en utilisant une analyse de d\u00e9pendance v\u00e9rifi\u00e9e et un sch\u00e9ma d’induction sp\u00e9cifique aux programmes ne contenant pas de cycle de d\u00e9pendance. On pr\u00e9sentera aussi la compilation de ces constructions, en montrant les adaptations n\u00e9cessaires aux sch\u00e9mas de compilation source \u00e0 source standard, et les invariants permettant de prouver la correction de ces sch\u00e9mas. Enfin, on expliquera pourquoi l’arri\u00e8re du compilateur doit \u00e9galement \u00eatre modifi\u00e9 pour compiler ces constructions efficacement.
<\/p>\n\n\n\n
M\u00e9canisation d’une s\u00e9mantique d\u00e9notationnelle dans un compilateur Lustre v\u00e9rifi\u00e9<\/strong>
Paul Jeanmaire (ENS, Inria)
September 12, 2023<\/em>
Dans cette pr\u00e9sentation, je d\u00e9crirai comment on impl\u00e9mente dans Coq une s\u00e9mantique d\u00e9notationnelle du langage Lustre et comment on prouve son \u00e9quivalence avec le mod\u00e8le relationnel existant dans le compilateur. Cette approche, constructive, permet de r\u00e9soudre le probl\u00e8me d’existence d’une s\u00e9mantique et facilite la preuve de certaines propri\u00e9t\u00e9s du langage.<\/p>\n\n\n\n
Fr\u00e9d\u00e9ric Gava, Universit\u00e9 Paris-Est Cr\u00e9teil
July 5, 2023<\/em>
Apr\u00e8s un bref rappel du mod\u00e8les BSP et de sa version hi\u00e9rarchique qu’est Multi-BSP, nous tenterons de r\u00e9pondre (formellement) \u00e0 une question d’apparence na\u00efve : qu\u2019est-ce qu\u2019un algorithme (multi-)BSP ? Pour ce faire, nous \u00e9tendrons \u00e0 BSP la d\u00e9finition axiomatique des algorithmes s\u00e9quentiels de Gurevich, Celle-ci se base sur les alg\u00e8bres \u00e9volutives aussi appel\u00e9es ASMs. Avec ces nouveaux postulats, nous obtenons alors la classe des algorithmes BSP. Puis nous donnerons une \u00e9quivalence algorithmique entre les algorithmes BSP et un mini langage imp\u00e9ratif prouvant que les langages de programmation BSP usuels sont algorithmiquement complet. Nous serons alors \u00e0 m\u00eame de d\u00e9finir ce qu\u2019est un algorithme Multi-BSP et sa caract\u00e9risation imp\u00e9rative. Nous terminerons par une discussion sur les limites de cette caract\u00e9risation imp\u00e9rative et du mod\u00e8le Multi-BSP. N.B. : Aucune connaissance pr\u00e9alable sur les ASMs n’est n\u00e9cessaire pour suivre cet expos\u00e9.<\/p>\n\n\n\n
Julien Tesson, Nomadic Labs
June 9, 2023<\/em>
Gestion d’un code source de grande taille avec git : l’exemple de Tezos.<\/p>\n\n\n\n
Thierry Lecomte, Clearsy
May 17, 2023<\/em>
Le d\u00e9veloppement d’applications s\u00fbres et s\u00e9curitaires requiert une large palette de techniques pour leur d\u00e9veloppement logiciel et mat\u00e9riel, ainsi que pour leur v\u00e9rification\/validation. L’expos\u00e9 pr\u00e9sente une solution technologique (https:\/\/www.clearsy.com\/outils\/clearsy-safety-platform\/) combinant un certain nombre de techniques, formelles ou non, comme:<\/p>\n\n\n\n\n
L’expos\u00e9 fait le point sur le cadre d’application (incluant les sp\u00e9cifications syst\u00e8me), le retour d’exp\u00e9rience, les travaux de recherche et d\u00e9veloppement en cours ainsi les probl\u00e8mes scientifiques et techniques ouverts. Les th\u00e9matiques couvertes incluent, \u00e0 des degr\u00e9s divers: la mod\u00e9lisation formelle, la g\u00e9n\u00e9ration de code et la compilation, la preuve math\u00e9matique, le deep-learning et la cybers\u00e9curit\u00e9, le tout sous le prisme de la certification normative.<\/p>\n\n\n\n
Simon Robillard, Universit\u00e9 de Montpellier
April 18, 2023<\/em>
Cette pr\u00e9sentation d\u00e9crit un cadre th\u00e9orique pour analyser et v\u00e9rifier des programmes contenant des boucles. Cette technique est bas\u00e9e sur un language de premier ordre et utilise des “expressions \u00e9tendues” qui permettent de d\u00e9crire \u00e0 la fois les propri\u00e9t\u00e9s fonctionnelles et les propri\u00e9t\u00e9s temporelles des boucles. Elle permet, en conjonction avec des prouveurs automatiques de th\u00e9or\u00e8mes existants, d’automatiser des t\u00e2ches telles que la v\u00e9rification de la correction partielle, la v\u00e9rification de la terminaison, et la g\u00e9n\u00e9ration d’invariants pour les boucles.<\/p>\n\n\n\n
Simon Robillard, Universit\u00e9 de Montpellier
April 17, 2023<\/em>
Les syst\u00e8mes informatiques occupent un r\u00f4le toujours croissant dans nos soci\u00e9t\u00e9s, et les d\u00e9fauts dans la conception ou l’impl\u00e9mentation de ces syst\u00e8mes peuvent avoir des cons\u00e9quences co\u00fbteuses. L’abstraction math\u00e9matique peut \u00eatre utilis\u00e9e pour obtenir des garanties fortes sur ces syst\u00e8mes. Ces techniques, regroup\u00e9es sous le terme de m\u00e9thodes formelles, sont largement comprises et encourag\u00e9es depuis plus de 50 ans, mais jusqu’\u00e0 r\u00e9cemment, la complexit\u00e9 des syst\u00e8mes \u00e0 v\u00e9rifier a emp\u00each\u00e9 leur application \u00e0 grande \u00e9chelle. Aujourd’hui, les techniques de d\u00e9duction automatique fournissent une r\u00e9ponse de plus en plus efficace \u00e0 ce d\u00e9fi. Des outils ciblant diverses logiques peuvent \u00eatre utilis\u00e9s pour raisonner au sujet de probl\u00e8mes math\u00e9matiques. Les probl\u00e8mes issus de la v\u00e9rification logicielle et mat\u00e9rielle sont, par leur nature, particuli\u00e8rement adapt\u00e9s au raisonnement automatique. Dans cette pr\u00e9sentation, je donnerai un aper\u00e7u des diff\u00e9rents outils de d\u00e9duction automatique, et leur application \u00e0 des probl\u00e8mes de v\u00e9rification.<\/p>\n\n\n\n
Adrien Guatto, Universit\u00e9 Paris Cit\u00e9, IRIF
April 12, 2023<\/em>
Travail men\u00e9 en collaboration avec Christine Tasson et Ada Vienot. La programmation fonctionnelle r\u00e9active traite de structures de donn\u00e9es infinies parcourues \u00e0 un rythme fix\u00e9. Ce rythme doit \u00eatre identique pour tous les producteurs et tous les consommateurs d’une m\u00eame structure. Dans cet expos\u00e9, je pr\u00e9senterai un langage th\u00e9orique dont les types d\u00e9crivent ces rythmes de parcours, et dont la gestion sous-structurelle des contextes assure l’accord des producteurs et des consommateurs.<\/p>\n\n\n\n
Julien Signoles, CEA
February 13, 2023<\/em>
Cet expos\u00e9 pr\u00e9sentera Frama-C, une plateforme open-source d\u00e9di\u00e9e \u00e0 l’analyse de programmes \u00e9crits en langage C. Apr\u00e8s un aper\u00e7u g\u00e9n\u00e9ral de la plateforme, nous introduirons ses principaux greffons d’analyse. Ainsi, nous expliquerons d’abord comment prouver l’absence de comportements ind\u00e9finis (ou les d\u00e9tecter s’il y en a) \u00e0 l’aide d’Eva, le greffon d’analyse de valeurs par interpr\u00e9tation abstraite, nous introduirons ensuite comment prouver des propri\u00e9t\u00e9s fonctionnelles \u00e0 l’aide du greffon WP d\u00e9di\u00e9 \u00e0 la v\u00e9rification d\u00e9ductive, puis nous pr\u00e9senterons comment d\u00e9tecter des erreurs avanc\u00e9es en cours d’ex\u00e9cution d’un programme, \u00e0 l’aide d’E-ACSL, le greffon d\u00e9di\u00e9 \u00e0 la v\u00e9rification \u00e0 l’ex\u00e9cution. Enfin, nous montrerons quelques usages plus avanc\u00e9s combinant diff\u00e9rentes analyses. Les diff\u00e9rentes techniques pr\u00e9sent\u00e9es seront illustr\u00e9es \u00e0 travers diff\u00e9rents exemples r\u00e9els provenant de domaines applicatifs vari\u00e9s (nucl\u00e9aire, avionique, carte \u00e0 puce, …).<\/p>\n\n\n\n
Jolan Philippe, IMT Atlantique
January 23, 2023<\/em>
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.<\/p>\n\n\n\n2022<\/h2>\n\n\n\n
Guillaume Cleuziou (LIFO, Universit\u00e9 d’Orl\u00e9ans & Universit\u00e9 de la Nouvelle-Cal\u00e9donie)
Fr\u00e9d\u00e9ric Loulergue (LIFO, Universit\u00e9 d’Orl\u00e9ans & Northern Arizona University)
April 25, 2022<\/em>
Dans cet expos\u00e9 nous vous pr\u00e9senterons comment pr\u00e9parer une mobilit\u00e9 hors de m\u00e9tropole et l’exp\u00e9rience de ces mobilit\u00e9s \u00e0 l’Universit\u00e9 de Nouvelle Cal\u00e9donie, et \u00e0 la Northern Arizona University.<\/p>\n\n\n\n
Benoit Gallet, Northern Arizona University
January 17, 2022<\/em>
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.<\/p>\n\n\n\n2021<\/h2>\n\n\n\n
Pierre R\u00e9ty, LIFO, Universit\u00e9 d’Orl\u00e9ans
November 22, 2021<\/em>
Un lecteur d\u2019\u00e9cran est un logiciel qui permet de naviguer et d\u2019agir sur les \u00e9l\u00e9ments graphiques sans regarder l\u2019\u00e9cran, et restitue les textes sous forme audio ou braille. Il permet ainsi aux personnes en difficult\u00e9 de lecture (mal-voyants, analphab\u00e8tes, dyslexiques) d\u2019utiliser l\u2019ordinateur ou le smartphone. Un lecteur d\u2019\u00e9cran appel\u00e9 VoiceOver est disponible en natif et gratuitement sur les produits Apple. Mais il pr\u00e9sente des anomalies et des limitations. Nous cherchons ici \u00e0 corriger les principaux d\u00e9fauts de VoiceOver, ce qu\u2019Apple ne fait pas, en relevant plusieurs d\u00e9fis. Comment am\u00e9liorer : – un logiciel \u00e0 sources ferm\u00e9es ? – la synth\u00e8se vocale ? – la navigation ? Nous apportons des r\u00e9ponses \u00e0 ces questions, ainsi qu\u2019une impl\u00e9mentation. Une d\u00e9monstration sera effectu\u00e9e.<\/p>\n\n\n\n
Nikolai Kosmatov, Thales Research & Technology (TRT)
March 15, 2021<\/em>
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.<\/p>\n\n\n\n
March 8, 2021<\/em>
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\u00e9d\u00e9ric Dadeau, Jean-Philippe Gros and Olga Kouchnarenko<\/p>\n\n\n\n
C\u00e9dric Eichler, INSA Centre Val de Loire, LIFO
February 15, 2021<\/em>
Les syst\u00e8mes distribu\u00e9s modernes \u00e9voluent dans des contextes soumis \u00e0 \u00e9volutions auxquelles ils doivent s’adapter. Ils doivent ainsi faire face \u00e0 l’arriv\u00e9e ou au d\u00e9part de composants, aux pannes, aux \u00e9volutions des besoins… L’informatique autonome fournit un cadre pour la d\u00e9l\u00e9gation de la gestion de ces (auto-)adaptations au syst\u00e8me lui-m\u00eame, limitant ou \u00e9liminant les interventions humaines. Ce s\u00e9minaire introductif pr\u00e9sentera dans un premier temps l’informatique autonome, son inception, ses objectifs, sa mise en \u0153uvre au travers de la boucle de contr\u00f4le MAPE-K, ainsi que quelques unes des probl\u00e9matiques qui lui sont associ\u00e9es. Dans un second temps, nous pr\u00e9senterons une approche de mod\u00e9lisation formelle de syst\u00e8mes auto-adaptatifs bas\u00e9e sur la r\u00e9\u00e9criture de graphe. Cette approche permet de repr\u00e9senter l’\u00e9tat d’un syst\u00e8me, ses \u00e9tats acceptables et ses adaptations. Finalement, nous verrons comment cette approche permet de sp\u00e9cifier des adaptations pr\u00e9servant n\u00e9cessairement la correction d’un syst\u00e8me.<\/p>\n\n\n\n
Jean Krivine, IRIF (joint work with Thomas Ehrhard (CNRS, IRIF) and Ying Jiang (ISCAS, China)
February 8, 2021<\/em>
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 \u201cimplemented\u201d by a fully compositional LTS semantics. I will argue that CBP offers an interesting tradeoff between calculi with a fixed communication topology \u00e0 la CCS and calculi with dynamic connectivity such as the \u03c0-calculus.<\/p>\n\n\n\n
Federico Olimpieri, LIPN
February 1, 2021<\/em>
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\u2019s 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.<\/p>\n\n\n\n
Simon Robillard et H\u00e9l\u00e8ne Coullon, IMT Atlantique
January 18, 2021<\/em>
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<\/p>\n","protected":false},"excerpt":{"rendered":"