Seminar

Seminars related to Épicure’s research themes:

• Épicure Seminar – internal only
• 68NQRT – http://68nqrt.irisa.fr/
• Sosysec – http://seminaire-dga.gforge.inria.fr/

Past sessions of the Épicure Seminar:

• 2023/04/06 Enzo Crance “Towards stratified parametricity for CCω” abstract
  Proof automation in Coq notoriously suffers from the expressivity of its dependently-typed programming language, especially the possibility to represent a same mathematical object with several data structures. In this talk, we will explore state-of-the-art techniques exploiting relations between types to derive information about more complex terms, and we will present 2 pre-processing tools exploiting this kind of knowledge to rewrite goals. The first one, Trakt, extends the input domains of SMT-like automation tactics thanks to embeddings between types. The second one, more general but still in progress, is based on a new flavour of parametricity called stratified parametricity, building on recent work inside the Gallinette team.
• 2023/03/30 Frédéric Bour “Engineering error messages for LR parsers” abstract
  LR parsing is a powerful technology that generates efficient parsers
  from a declarative specification and guarantees the absence of
  ambiguities. However, the parsers produced fall short when provided with
  incorrect input: generally, only the location of the erroneous construct
  can be reported. LRgrep aims to enhance LR(1) parsers with good error
  messages. It takes the form of a DSL that complements the grammar with a
  specification of error messages. Tools can check that all errors are
  covered and help to keep the error messages relevant when the grammar
  evolves. We demonstrate it on the OCaml grammar.
• 2023/03/16 Yannick Zakowski “Monadic Definitional Interpreters as Formal Semantic Models of Computations in Coq” abstract
  Monadic interpreters have seen in recent years a rise in popularity as a means to model and reason about impure computations in dependently typed theories. The Interaction Tree project in particular implements a set of libraries in the Coq proof assistant providing tools to enable this approach at scale.This talk intents to paint an overview of the project. I will first introduce the core concepts: modelling divergence through coinduction, achieving modularity through layered interpreters in the style of algebraic effects, enabling testing by extraction, and offering equational and Hoare-style relational reasoning up-to a notion of weak bisimilarity.
  Projects to which the approach have been applied, notably in the modelling of LLVM IR as part of the Vellvm project, will be mentioned on the way.

  Through the second half of the presentation, I will focus more specifically on so-called Choice Trees, a recent proposal to provide in this ecosystem a proper support for non-deterministic computations.

• 2023/03/09 Basile Clément “Prophetic Annotations: A Different Take on Translation-Validation” abstract
  Tensor compilers transform high-level mathematical specifications on (mostly) pure multidimensional arrays, called tensors, down to low-level imperative code with mutable arrays and loops, tailored to specific hardware. These compilers are mostly out of reach of traditional translation-validation techniques due to the structure-modifying transformations they perform.In this talk, I will present the results of my PhD research on a translation-validation technique for tensor compilers that is centered around the idea of _prophetic annotations_ : lightweight compiler-generated annotations inspired by the polyhedral model that do not encode transformations but rather link imperative array accesses to the original pure value the compiler believes they represent in the original specification.

  After a quick presentation of tensor compilers and the motivations for their use, I will present the techniques developed in my thesis for the validation of a subset of the transformations performed by these compilers that include both affine transformations and local algebraic transformations. I will show experimental results of the approach on the industrial-grade Halide compiler, and briefly present unfinished extensions that would allow the approach to handle a larger class of programs and transformations, including most common uses of non-affine programs and transformations as well as handling of commutative-associative reductions. Finally, I will present some thoughts on the way this work separates affine from non-affine annotations, and the potential uses of this approach to provide lightweight specifications for the verification of numerical programs.

• 2023/03/02 Simon Castellan, Action Exploratoire Inria “Back to the trees”
• 2023/02/06 Son Ho, “Aeneas: Rust Verification by Functional Translation” abstract
  We present Aeneas, a new verification toolchain for Rust programs
  based on a lightweight functional translation. We leverage Rust’s rich
  region-based type system to eliminate memory reasoning for a large
  class of Rust programs by translating them to a pure lambda-calculus,
  as long as they do not rely on interior mutability or unsafe code.
  Doing so, we relieve the proof engineer of the burden of memory-based
  reasoning, allowing them to instead focus on *functional* properties
  of their code.
• 2023/01/26 Vincent Rébiscoul, “Analyses Statiques pour Sémantiques Squelettiques” abstract
  Dans cette présentation, nous décrivons une méthode pour définir une interprétation abstraite correcte à partir d’une description formelle de sémantique d’un langage de programmation: une Sémantique Squelettique. Nous ajoutons une notion de points de programme aux sémantiques squelettiques pour différencier des morceaux de programme syntaxiquement équivalents mais qui se trouve à des endroits différents. Nous proposons une méthodologie pour dériver une interprétation abstraite à partir d’une sémantique squelettique qui est correcte par construction. Nous appliquons notre méthode pour définir une analyse d’intervalle pour un petit language impératif.
• 2023/01/12 Pierre Lermusiaux, “Analyse statique de transformations pour l’élimination de motifs” abstract
  Thèse effectuée au Loria sous la direction de Pierre-Étienne Moreau et Horatiu Cirstea.Ma thèse propose une étude formelle des procédures de transformation de programmes dans le but d’exprimer et de garantir des propriétés syntaxiques sur le comportement et les résultats d’une telle transformation. Dans le contexte de la vérification formelle des programmes, il est en effet souvent nécessaire de pouvoir caractériser la forme des termes obtenus par réduction suivant une transformation considérée. Dans le contexte de langages typés, le système de type peut permettre de spécifier et de vérifier certaines caractéristiques sur la forme de ces termes, en explicitant notament leur symboles constructeurs. Il est cependant souvent intéressant de pouvoir spécifier l’absence de certains symboles, ou de certains motifs.J’introduit, dans ma thèse, un formalisme, basé sur les notions de filtrage par motif et de réécriture, permettant de décrire de telles propriétés. Le formalisme proposé repose sur un système d’annotations des symboles de fonction décrivant une spécification du comportement attendu des fonctions associées. On présente alors une méthode d’analyse statique permettant de vérifier que les transformations étudiées, exprimées par un système de réécriture, satisfont en effet ces spécifications.
• 2022/12/14 Frédéric Besson, “An eBPF backend for CompCert”
• 2022/11/28 Santiago Bautista, “Lifting Numeric Relational Domains to Algebraic Data Types”
• 2022/11/09 Frédéric Besson, “An extension of CompCert that allows to call binary code”
• 2022/10/26 Léo Gourdin, “Formally verified block optimizations by symbolic execution modulo invariants” abstract
  CompCert (ACM Software System Award 2021) is the first industrial-strength compiler with a mechanically checked proof of correctness. But CompCert remains a moderately optimizing C compiler. Indeed, some optimizations of “gcc -O1” like Lazy Code Motion (LCM) or Strength Reduction (SR) are still missing: developing these efficient optimizations together with their formal proofs remains challenging.
  We already combined formally verified translation validators for certifying the results of an efficient superblock scheduler with peephole optimizations. We now revisit and generalize this approach into a framework (integrated in CompCert) able to validate many more optimizations: an enhanced superblock scheduler, but also Dead Code Elimination (DCE), Constant Propagation (CP), and more noticeably, LCM and SR global transformations.
  Toward this goal, we introduce a new intermediate representation (IR) named BTL, which syntactically represents blocks of code. Then, we propose a block-based symbolic execution framework capable of aggregating “local” simulations at the global level, making sure that the changes are consistent between blocks.
• 2022/09/28 Thomas Genet, “Comprendre Ethereum/Solidity par la pratique”
• 2022/09/21 Roméo La Spina (Inria Épicure), “Un analyseur flots de données pour le compilateur formellement vérifié CompCert” abstract
  Un compilateur vérifié est un compilateur accompagné d’une preuve qui montre que ce dernier n’introduit pas de bogue dans les programmes. Une référence du domaine est le compilateur CompCert du langage C, entièrement écrit et prouvé à l’aide de l’assistant de preuve Coq. CompCert est un compilateur non seulement vérifié, mais aussi optimisant ; ses performances en termes de temps d’exécution d’un programme compilé sont comparables à celles obtenues avec l’option `-O1` du compilateur de référence GCC (non vérifié).Plusieurs optimisations de CompCert utilisent une analyse flot de données, qui résout un ensemble d’équations grâce à un algorithme dû à Kildall. Cependant, selon la taille du treillis utilisé pour faire l’analyse, la convergence de l’algorithme peut nécessiter un temps extrêmement long. Un autre algorithme, développé par Bourdoncle, qui paramètre l’analyse par un ordre d’itération calculé au préalable, permet l’utilisation efficace d’opérateurs d’élargissement, solution classique pour pallier ce problème dans le domaine de l’interprétation abstraite. Nous avons donc choisi d’implémenter l’algorithme de Bourdoncle dans CompCert et de comparer ses performances à celles de l’algorithme de Kildall, à la fois en termes d’efficacité et en termes de précision de l’analyse.

Previously, at the Épicure seminar:

• 2021-2022
• 2020-2021