Search

National audience; L'arithmétique flottante est connue pour être un sujet difficile. Ses propriétés contreintuitives rendent l'écriture d'algorithmes manipulant les nombres flottants propice à de nombreuses erreurs. Des outils automatiques pour la vérification de programmes flottants existent mais ces outils faisant eux-mêmes usage de calculs en arithmétique flottante, on peut se poser la question de leur propre fiabilité. Dans cet article, nous proposons de vérifier formellement l'implémentation de raisonnements sur les nombres flottants dans le solveur de contraintes Colibri2. En particulier, nous présentons une méthodologie pour mener la preuve de correction de propagateurs de contraintes en utilisant l'assistant de preuve Coq. Nous discutons également de l'intégration des raisonnements prouvés à un développement logiciel complet en OCaml.

Mikino is a simple induction engine over transition systems. It is written in Rust, with a strong focus on ergonomics and user-friendliness. It is accompanied by a detailed tutorial which introduces basic notions such as logical operators and Smt solvers. Mikino and its companion tutorial target developers with little to no experience with verification in general and induction in particular. This work is an attempt to educate developers on what a proof by induction is, why it is relevant for program verification, why it can fail to (dis)prove a candidate invariant, and what to do in this case.

L'assistant de preuve Coq dispose d'une fonctionnalité permettant à l'utilisateur de dénir ses propres notations avec une grande souplesse. Dans ce cadre, les constantes numériques étaient initialement interprétées et achées par du code dédié dans des plugins OCaml. Depuis Coq 8.9 (janvier 2019), la commande Numeral Notation (aujourd'hui renommée Number Notation) permet d'implémenter ces parsers et printers de constantes numériques directement dans Coq. Suite entre autre à l'introduction des ottants primitifs, cette commande a depuis connue un certain nombre d'extensions qui seront présentées dans cette démonstration : valeurs à virgules ou exposant, valeurs hexadécimales, interprétation vers des types inductifs paramétrés ou non inductifs.

National audience; Dans un assistant de preuve comme Coq, un même objet mathématique peut souvent être formalisé par différentes structures de données. Par exemple, le type Z des entiers binaires, dans la bibliothèque standard de Coq, représente les entiers relatifs tout comme le type ssrint, des entiers unaires, fourni par la bibliothèque MathComp. En pratique, cette situation familière en programmation est un frein à la preuve formelle automatique. Dans cet article, nous présentons trakt, un outil dont l'objectif est de faciliter l'accès des utilisateurs de Coq aux tactiques d'automatisation, pour la représentation des théories décidables de leur choix. Cet outil construit une formule auxiliaire à partir d'un but utilisateur, et une preuve que cette dernière implique ce but initial. La formule auxiliaire est conçue pour être adaptée aux outils de preuve automatique (lia, SMTCoq, etc). Cet outil est extensible, grâce à une API permettant à l'utilisateur de définir plusieurs natures de plongements dans un jeu de structures de données de référence. Le méta-langage Coq-Elpi, utilisé pour l'implémentation, fournit des facilités bienvenues pour la gestion des lieurs et la mise en oeuvre des parcours de termes en jeu dans ces tactiques.

National audience; Cet article présente un système de vérification et d'inférence statique des tailles de tableaux dans un langage fonctionnel strict statiquement typé. Plutôt que de s'en remettre à des types dépendants, nous proposons un système de types proche de celui de ML. Le polymorphisme sert à définir des fonctions génériques en type et en taille. L'inférence permet une écriture plus légère des opérations classiques de traitement du signal-application point-à-point, accumulation, projection, transposée, convolution-et de leur composition ; c'est un atout clef de la solution proposée. Pour obtenir un bon compromis entre expressivité du langage des tailles et décidabilité de la vérification et de l'inférence, notre solution repose sur deux éléments : (i) un langage de types où les tailles sont des polynômes multi-variés et (ii) l'insertion de points de coercition explicites entre tailles dans le programme source. Lorsque le programme est bien typé, il s'exécute sans erreur de taille en dehors de ces points de coercition. Deux usages de la proposition faite ici peuvent être envisagés : (i) la génération de code défensif aux points de coercition ou, (ii) pour les applications critiques ou intensives, la vérification statique des coercitions en les limitant à des expressions évaluables à la compilation ou par d'autres moyens de vérification formelle. L'article définit le langage d'entrée, sa sémantique dynamique, son système de types et montre sa correction. Il est accompagné d'une implémentation en OCaml, dont le code source est accessible publiquement.

Lustre is a synchronous dataflow language designed for programming embedded systems. In the Vélus project, we use Coq to develop and formalize a compiler that accepts a normalized form of the language and produces imperative code. While this restricted form is suitable for code generated from a user interface based on block diagrams, we wanted to allow programmers to use thecomplete language.In this article, we present the normalization pass that transforms the complete language into the normalized one. This transformation is divided into three steps so as to simplify the correctness proofs. To show that the semantics is preserved, it is necessary to prove that the three steps preserve certain static and dynamic properties of the language. In particular, the relation between the clock types and the dynamic semantic must be established., Lustre est un langage synchrone à flots de données conçu pour programmer des systèmes embarqués. Dans le cadre du projet Vélus, nous avons développé et formalisé dans Coq un compilateur qui accepte une forme normalisée du langage et la compile vers du code impératif. Si cette forme réduite prend en charge un code généré depuis une interface utilisateur basée sur les schémas-blocs, nous voulons offrir au programmeur la possibilité de manipuler le langage complet.Dans cet article nous présentons l'étape de normalisation, qui transforme le langage de programmation en langage normalisé. Cette transformation est décomposée en trois étapes afin de simplifier les preuves de correction. Pour établir la préservation de la sémantique, il est nécessaire de démontrer que les trois passes préservent certaines propriétés statiques et dynamiques du langage. En particulier, il faut prouver le lien entre le typage des horloges et la sémantique dynamique pour pouvoir raisonner sur la suite de la compilation.

Timed automata (TAs) are a widely used formalism to specify systems having temporal requirements. However, exactly specifying the system may be difficult, as the user may not know the exact clock constraints triggering state transitions. In this work, we assume the user already specified a TA, and (s)he wants to validate it against an oracle that can be queried for acceptance. Under the assumption that the user only wrote wrong guard transitions (i.e., the structure of the TA is correct), the search space for the correct TA can be represented by a Parametric Timed Automaton (PTA), i.e., a TA in which some constants are parametrized. The paper presents a process that i) abstracts the initial (faulty) TA tainit in a PTA pta; ii) generates some test data (i.e., timed traces) from pta; iii) assesses the correct evaluation of the traces with the oracle; iv) uses the IMITATOR tool for synthesizing some constraints phi on the parameters of pta; v) instantiate from phi a TA tarep as final repaired model. Experiments show that the approach is successfully able to partially repair the initial design of the user., Comment: This is the author (and slightly extended) version of the manuscript of the same name published in the proceedings of the 13th International Conference on Tests and Proofs (TAP 2019). This version contains some additional explanations and all proofs