Search

Your search keyword '"Chantal Keller"' showing total 68 results
Start Over Author "Chantal Keller"
68 results on '"Chantal Keller"'

1. Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)

Author

Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J. Reynolds, and Cesare Tinelli

Subjects
Mathematics, QA1-939, Electronic computers. Computer science, QA75.5-76.95
Abstract

This extended abstract reports on current progress of SMTCoq, a communication tool between the Coq proof assistant and external SAT and SMT solvers. Based on a checker for generic first-order certificates implemented and proved correct in Coq, SMTCoq offers facilities both to check external SAT and SMT answers and to improve Coq's automation using such solvers, in a safe way. Currently supporting the SAT solver zChaff, and the SMT solver veriT for the combination of the theories of congruence closure and linear integer arithmetic, SMTCoq is meant to be extendable with a reasonable amount of effort: we present work in progress to support the SMT solver CVC4 and the theory of bit vectors.

Published
2016
Full Text
View/download PDF

14. Dependent types and multi-monadic effects in F.

Author

Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella Béguelin

Published
2016
Full Text
View/download PDF

25. SMTCoq: Mixing Automatic and Interactive Proof Technologies

Author

Chantal Keller

Subjects
Conjecture, Computer science, Programming language, business.industry, Proof assistant, Modular design, computer.software_genre, Mathematical proof, Formal proof, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Satisfiability modulo theories, Plug-in, Boolean satisfiability problem, business, computer
Abstract

SMTCoq is a plugin for the Coq interactive theorem prover to work in conjunction with automated theorem provers based on Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT), in an efficient and expressive way. As such, it allows one to formally establish, in a proof assistant, mathematical results relying on large combinatorial properties that require automatic Boolean reasoning. To this end, the huge SAT proofs coming from such problems can be safely checked in Coq and combined with standard mathematical Coq developments in a generic and modular way, for instance to obtain a formal proof of the Erdős Discrepancy Conjecture. To achieve this objective with the same degree of safety as Coq itself, SMTCoq communicates with SAT and SMT solvers that, in addition to a yes/no answer, can output traces of their internal proof search. The heart of SMTCoq is thus a certified, efficient and modular checker for such traces expressed in a format that can encompass most aspects of SMT reasoning. Preprocessors—that need not be certified—for proof traces coming from the state-of-the-art SMT solvers CVC4 and veriT and SAT solvers zChaff and Glucose are implemented. Coq can thus work in conjunction with widely used provers. From a proof assistant perspective, SMTCoq also provides a mechanism to let Coq users enjoy automation provided by external provers.

Published
2019
Full Text
View/download PDF

26. Tests and Proofs : 13th International Conference, TAP 2019, Held As Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October 9–11, 2019, Proceedings

Author

Dirk Beyer, Chantal Keller, Dirk Beyer, and Chantal Keller

Subjects
Software engineering, Compilers (Computer programs), Computer science, Machine theory, Electronic digital computers—Evaluation
Abstract

This book constitutes the refereed proceedings of the 13th International Conference on Tests and Proofs, TAP 2019, held as part of the Third World Congress on Formal Methods 2019, Porto, Portugal, in October 2019. The 10 regular papers and 2 invited paper presented in this volume were carefully reviewed and selected from 19 submissions. The TAP conference promotes research in verification and formal methods that targets the interplay of proofs and testing: the advancement of techniques of each kind and their combination, with the ultimate goal of improving software and system dependability.

Published
2019

27. A Coq formalisation of SQL's execution engines

Author

Eunice Martins, Véronique Benzaken, Chantal Keller, Evelyne Contejean, Vérification d'Algorithmes, Langages et Systèmes (LRI) (VALS - LRI), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), and ANR-15-CE39-0009,DataCert,Spécification intensive en Coq d'intégration de données orientée sécurité(2015)

Subjects
SQL, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Computer science, Programming language, Semantics (computer science), Proof assistant, InformationSystems_DATABASEMANAGEMENT, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 02 engineering and technology, Relational algebra, computer.software_genre, Oracle, Relational database management system, 020204 information systems, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, 0202 electrical engineering, electronic engineering, information engineering, Layer (object-oriented design), computer, Implementation, computer.programming_language
Abstract

International audience; In this article, we use the Coq proof assistant to specify and verify the low level layer of SQL's execution engines. To reach our goals, we first design a high-level Coq specification for data-centric operators intended to capture their essence. We, then, provide two Coq implementations of our specification. The first one, the physical algebra, consists in the low level operators found in systems such as Postgresql or Oracle. The second, SQL algebra, is an extended relational algebra that provides a semantics for SQL. Last, we formally relate physical algebra and SQL algebra. By proving that the physical algebra implements SQL algebra, we give high level assurances that physical algebraic and SQL algebra expressions enjoy the same semantics. All this yields the first, to our best knowledge, formalisation and verification of the low level layer of an RDBMS as well as SQL's compilation's physical optimisation: fundamental steps towards mechanising SQL's compilation chain.

Published
2018
Full Text
View/download PDF

28. Beagle as a HOL4 external ATP method

Author

Cezary Kaliszyk, Thibault Gauthier, Chantal Keller, Michael Norrish, Leopold Franzens Universität Innsbruck - University of Innsbruck, Programming securely with cryptography (PROSECCO), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Microsoft Research - Inria Joint Centre (MSR - INRIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Microsoft Research Laboratory Cambridge-Microsoft Corporation [Redmond, Wash.], NICTA Canberra labs, National ICT Australia [Sydney] (NICTA), University of Innsbruck, and Keller, Chantal

Subjects
Engineering, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Programming language, business.industry, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], HOL, 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, Translation (geometry), computer.software_genre, 01 natural sciences, Beagle, 010201 computation theory & mathematics, 0202 electrical engineering, electronic engineering, information engineering, business, Algorithm, computer, TRACE (psycholinguistics)
Abstract

This paper presents BEAGLE TAC, a HOL4 tactic for using Beagle as an external ATP fordischarging HOL4 goals. We implement a translation of the higher-order goals to the TFAformat of TPTP and add trace output to Beagle to reconstruct the intermediate steps derivedby the ATP in HOL4. Our translation combines the characteristics of existing successfultranslations from HOL to FOL and SMT-LIB, however we needed to adapt certain stagesof the translation in order to benefit form the expressivity of the TFA format and the powerof Beagle. In our initial experiments, we demonstrate that our system can prove, withoutany arithmetic lemmas, 81% of the goals solved by Metis.

Published
2018
Full Text
View/download PDF

29. SMTCoq: A Plug-In for Integrating SMT Solvers into Coq

Author

Clark Barrett, Chantal Keller, Andrew Reynolds, Burak Ekici, Cesare Tinelli, Alain Mebsout, Guy Katz, University of Iowa [Iowa City], Université Paris-Saclay, Laboratoire de Recherche en Informatique (LRI), CentraleSupélec-Université Paris-Sud - Paris 11 (UP11)-Centre National de la Recherche Scientifique (CNRS), Vérification d'Algorithmes, Langages et Systèmes (LRI) (VALS - LRI), CentraleSupélec-Université Paris-Sud - Paris 11 (UP11)-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université Paris-Sud - Paris 11 (UP11)-Centre National de la Recherche Scientifique (CNRS), Université Paris-Sud - Paris 11 (UP11), Stanford University, Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), and Keller, Chantal

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Programming language, Computer science, business.industry, Proof assistant, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 02 engineering and technology, Uninterpreted function, computer.software_genre, Propositional calculus, Automation, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Fragment (logic), TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Extensionality, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Plug-in, Boolean satisfiability problem, business, computer
Abstract

International audience; This paper describes SMTCoq, a plug-in for the integration of external solvers into the Coq proof assistant. Based on a checker for generic first-order proof certificates fully implemented and proved correct in Coq, SMTCoq offers facilities to check answers from external SAT and SMT solvers and to increase Coq's automation using such solvers, all in a safe way. The current version supports proof certificates produced by the SAT solver ZChaff, for propositional logic, and the SMT solvers veriT and CVC4, for the quantifier-free fragment of the combined theory of fixed-size bit vectors, functional arrays with extensionality, linear integer arithmetic, and uninterpreted function symbols.

Published
2017
Full Text
View/download PDF

30. A Symbolic Operational Semantics for TESL

Author

Chantal Keller, Thibaut Balabonski, Frédéric Boulanger, Burkhart Wolff, Benoît Valiron, and Hai Nguyen Van

Subjects
Set (abstract data type), Theoretical computer science, Computer science, Synchronicity, Synchronization (computer science), 0202 electrical engineering, electronic engineering, information engineering, System testing, 020207 software engineering, 020201 artificial intelligence & image processing, The Symbolic, 02 engineering and technology, Operational semantics, TRACE (psycholinguistics)
Abstract

TESL addresses the specification of the temporal aspects of an architectural composition language that allows the composition of timed subsystems. TESL specifies the synchronization points between events and time scales. Methodologically, subsystems having potentially different models of execution are abstracted to their interfaces expressed in terms of timed events. In this paper, we present an operational semantics of TESL for constructing symbolic traces that can be used in an online-test scenario: the symbolic trace containing a set of constraints over time-stamps and occurrences of events is matched against concrete runs of the system. We present the operational rules for building symbolic traces and illustrate them with examples. Finally, we show a prototype implementation that generates symbolic traces, and its use for testing.

Published
2017
Full Text
View/download PDF

31. Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)

Author

Andrew Reynolds, Cesare Tinelli, Alain Mebsout, Guy Katz, Chantal Keller, Burak Ekici, University of Iowa [Iowa City], Stanford University, Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Jasmin Christian Blanchette, and Cezary Kaliszyk

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Integer arithmetic, Computer science, 02 engineering and technology, Certification, computer.software_genre, lcsh:QA75.5-76.95, Satisfiability modulo theories, 0202 electrical engineering, electronic engineering, information engineering, business.industry, Programming language, lcsh:Mathematics, Proof assistant, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Work in process, lcsh:QA1-939, Automation, Logic in Computer Science (cs.LO), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, 020201 artificial intelligence & image processing, Congruence closure, lcsh:Electronic computers. Computer science, business, Boolean satisfiability problem, computer
Abstract

This extended abstract reports on current progress of SMTCoq, a communication tool between the Coq proof assistant and external SAT and SMT solvers. Based on a checker for generic first-order certificates implemented and proved correct in Coq, SMTCoq offers facilities both to check external SAT and SMT answers and to improve Coq's automation using such solvers, in a safe way. Currently supporting the SAT solver zChaff, and the SMT solver veriT for the combination of the theories of congruence closure and linear integer arithmetic, SMTCoq is meant to be extendable with a reasonable amount of effort: we present work in progress to support the SMT solver CVC4 and the theory of bit vectors., In Proceedings HaTT 2016, arXiv:1606.05427

Published
2016

32. Typeful Normalization by Evaluation

Author

Olivier Danvy and Chantal Keller and Matthias Puech, Danvy, Olivier, Keller, Chantal, Puech, Matthias, Olivier Danvy and Chantal Keller and Matthias Puech, Danvy, Olivier, Keller, Chantal, and Puech, Matthias

Abstract

We present the first typeful implementation of Normalization by Evaluation for the simply typed lambda-calculus with sums and control operators: we guarantee type preservation and eta-long (modulo commuting conversions), beta-normal forms using only Generalized Algebraic Data Types in a general-purpose programming language, here OCaml; and we account for sums and control operators with Continuation-Passing Style. First, we implement the standard NbE algorithm for the implicational fragment in a typeful way that is correct by construction. We then derive its call-by-value continuation-passing counterpart, that maps a lambda-term with sums and call/cc into a CPS term in normal form, which we express in a typed dedicated syntax. Beyond showcasing the expressive power of GADTs, we emphasize that type inference gives a smooth way to re-derive the encodings of the syntax and typing of normal forms in Continuation-Passing Style.

Published
2015
Full Text
View/download PDF

33. A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses

Author

Chantal Keller, Benjamin Grégoire, Benjamin Werner, Germain Faure, Laurent Théry, Michael Armand, Mathematical, Reasoning and Software (MARELLE), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Types, Logic and computing (TYPICAL), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Inria Saclay - Ile de France, Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), Jouannaud, Jean-Pierre and Shao, Zhong, ANR- 08-DEFIS-005-01,DECERT,Déduction certifiée(2008), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), and ANR-08-EMER-0005,DECERT,Déduction Certifiée(2008)

Subjects
Soundness, Computer science, Programming language, business.industry, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, Modular design, Conjunctive normal form formula, Mathematical proof, computer.software_genre, 01 natural sciences, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, Satisfiability modulo theories, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, 0202 electrical engineering, electronic engineering, information engineering, Linear arithmetic, Conjunctive normal form, Boolean satisfiability problem, business, computer
Abstract

International audience; We present a way to enjoy the power of SAT and SMT provers in Coq without compromising soundness. This requires these provers to return not only a yes/no answer, but also a proof witness that can be independently rechecked. We present such a checker, written and fully certified in Coq. It is conceived in a modular way, in order to tame the proofs' complexity and to be extendable. It can currently check witnesses from the SAT solver ZChaff and from the SMT solver veriT. Experiments highlight the efficiency of this checker. On top of it, new reflexive Coq tactics have been built that can decide a subset of Coq's logic by calling external provers and carefully checking their answers.

Published
2011
Full Text
View/download PDF

34. Parametricity in an Impredicative Sort

Author

Chantal Keller and Marc Lasson, Keller, Chantal, Lasson, Marc, Chantal Keller and Marc Lasson, Keller, Chantal, and Lasson, Marc

Abstract

Reynold's abstraction theorem is now a well-established result for a large class of type systems. We propose here a definition of relational parametricity and a proof of the abstraction theorem in the Calculus of Inductive Constructions (CIC), the underlying formal language of Coq, in which parametricity relations' codomain is the impredicative sort of propositions. To proceed, we need to refine this calculus by splitting the sort hierarchy to separate informative terms from non-informative terms. This refinement is very close to CIC, but with the property that typing judgments can distinguish informative terms. Among many applications, this natural encoding of parametricity inside CIC serves both theoretical purposes (proving the independence of propositions with respect to the logical system) as well as practical aspirations (proving properties of finite algebraic structures). We finally discuss how we can simply build, on top of our calculus, a new reflexive Coq tactic that constructs proof terms by parametricity.

Published
2012
Full Text
View/download PDF

35. HOL-TestGen Version 1.8 USER GUIDE

Author

Achim Brucker, Lukas Brügger, Abderrahmane Feliachi, Chantal Keller, Matthias Krieger, Delphine Longuet, Yakoub Nemouchi, Frédéric Tuong, Burkhart Wolff, Institute of Information Security [ETH Zürich], Department of Computer Science [ETH Zürich] (D-INFK), Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich)- Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich), Department of Biosystems Science and Engineering [ETH Zürich] (D-BSSE), Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich), Laboratoire de Recherche en Informatique (LRI), CentraleSupélec-Université Paris-Sud - Paris 11 (UP11)-Centre National de la Recherche Scientifique (CNRS), Université Paris-Sud - Paris 11 (UP11), Centre National de la Recherche Scientifique (CNRS), CentraleSupélec, Université Paris-Saclay, IRT SystemX (IRT SystemX), Univeristé Paris-Saclay, and LRI - CNRS, University Paris-Sud

Subjects
[SCCO.COMP]Cognitive science/Computer science

38. Bécassine à la chasse au Coq (démonstration)

Author

Blot, Valentin, Dubois de Prisque, Louise, Keller, Chantal, Vial, Pierre, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Chantal Keller, and Timothy Bourke

Subjects
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

National audience; Nous présentons une nouvelle tactique Coq (snipe) permettant de prouver automatiquement des butsCoq en les envoyant à des prouveurs automatiques externes du premier ordre via des plugins. Pour ce faire, la tactique snipe réduit le but à un énoncé du premier ordre et enrichit le contexte local avec des énoncés explicitant pour le prouveur la sémantique du but. Nous combinons des transformations modulaires et indépendantes permettant chacune de réduire un aspect spécifique du langage de Coq au langage (plussimple) d’un prouveur automatique. A l’heure actuelle, snipe utilise des transformations simples mais cruciales qui explicitent des définitions et des types algébriques. Ceci permet de prouver automatiquementdes buts mêlant raisonnement au premier ordre, types de données et polymorphisme. Ce prototype de tactique automatique est un premier pas vers l’implantation et la combinaison de transformations plus complexes, qui rendront Coq plus facile d’accès.

Published
2022

39. Inférence parallèle pour un langage réactif probabiliste

Author

Baudart, Guillaume, Mandel, Louis, Pouzet, Marc, Tekin, Reyyan, Parallélisme de Kahn Synchrone ( Parkas), Département d'informatique - ENS Paris (DI-ENS), École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), IBM Watson Research Center, IBM, Chantal Keller, and Timothy Bourke

Subjects
[INFO]Computer Science [cs]
Abstract

National audience; ProbZelus est un langage synchrone probabiliste qui permet de décrire des modèles probabilistes réactifs en interaction avec un environnement observable. Des méthodes d'inférences réactives permettent d'apprendre en ligne les distributions associées aux paramètres non-observés du modèle à partir d'observations statistiques. Ce problème n'a, en général, pas de solution analytique simple. Pour obtenir des estimations précises, une méthode classique consiste à analyser les résultats obtenus par de nombreuses exécutions indépendantes du modèle. Ces méthodes sont coûteuses, mais ont l'avantage de pouvoir être massivement parallélisées. Nous proposons d'utiliser JAX pour paralléliser les méthodes d'inférence réactive de ProbZelus. JAX est une bibliothèque récente qui permet de paralléliser automatiquement du code Python qui peut ensuite être exécuté de manière efficace et transparente sur CPU, GPU, ou TPU. Dans cet article, nous décrivons un nouveau moteur d'inférence réactive parallèle implémenté en JAX et le nouveau backend JAX associé pour ProbZelus. Nous montrons sur des exemples existants que notre nouvelle implémentation surpasse l'implémentation séquentielle originale pour un nombre de particules élevé.

Published
2022

40. Connecter l'écosystème OCaml à Software Heritage via opam

Author

Andrès, Léo, Boujbel, Raja, Gesbert, Louis, Pinto, Dario, OCamlPro SAS, Université Paris-Saclay, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Chantal Keller, and Timothy Bourke

Subjects
[INFO]Computer Science [cs]
Abstract

National audience; Software Heritage est un projet initié par Inria ayant pour but d'archiver l'ensemble des logiciels libres disponibles sur internet. Dans cet article nous présentons Software Heritage et décrivons nos travaux en lien avec l'écosystème OCaml, opam et Software Heritage. Ces travaux comprennent notamment l'ajout à Software Heritage de modules permettant l'archivage des paquets présents sur opam, le développement d'une bibliothèque OCaml permettent de travailler avec les identifiants Software Heritage, l'ajout à opam de la possibilité de récupérer sur Software Heritage des paquets qui ne sont plus disponibles et enfin la correction du dépôt opam officiel afin de retrouver les paquets déjà manquants. Aujourd'hui, 3516 paquets opam sont déjà archivés sur Software Heritage.

Published
2022

41. Formalising Futures and Promises in Viper

Author

Giusto, Cinzia, Germerie Guizouarn, Loïc, Henrio, Ludovic, Lozes, Etienne, Université Côte d'Azur (UCA), Compilation et Analyse, Logiciel et Matériel (CASH), Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Lyon, Institut National de Recherche en Informatique et en Automatique (Inria), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Chantal Keller, Timothy Bourke, and ANR-17-EURE-0004,UCA DS4H,UCA Systèmes Numériques pour l'Homme(2017)

Subjects
[INFO]Computer Science [cs]
Abstract

National audience; Futures and promises are respectively a read-only and a write-once pointer to a placeholder in memory. They are used to transfer information between threads in the context of asynchronous concurrent programming. Futures and promises simplify the implementation of synchronisation mechanisms between threads. Nonetheless they can be error prone as data races may arise when references are shared and transferred. We aim at providing a formal tool to detect those errors. Hence, in this paper we propose a proof of concept by implementing the future/promise mechanism in Viper: a verification infrastructure, that provides a way to reason about resource ownership in programs.

Published
2022

42. Démonstration de Steel, une logique de séparation concurrente pour prouver des programmes F* (démonstration)

Author

Fromherz, Aymeric, Reitz, Antonin, Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Chantal Keller, Timothy Bourke, and Bourke, Timothy

Subjects
[INFO]Computer Science [cs], [INFO] Computer Science [cs]
Abstract

National audience; Steel est un framework pour développer et prouver des programmes concurrents écrits en F , un langage de programmation avec types dépendants ainsi qu'un assistant de preuve. Inspiré par Iris, Steel repose sur une logique de séparation concurrente imprédicative qui inclut un modèle mémoire fondé sur des monoïdes commutatifs partiels et permet l'utilisation d'invariants alloués dynamiquement pour raisonner sur des interactions concurrentes sans recourir à des verrous ("locks"). Afin d'offrir une vérification semi-automatique, Steel sépare les obligations de preuves générées en deux parties : une procédure de décision partielle, implémentée à l'aide du moteur de tactiques de F , raisonne sur la logique de séparation tandis qu'un solveur SMT permet de décharger automatiquement des obligations de preuves exprimées en logique du premier ordre, par exemple liées à de l'arithmétique. Dans cette démonstration, nous présentons plusieurs bibliothèques vérifiées qui illustrent l'expressivité et la programmabilité de Steel.

Published
2022

43. Jouez à Faire Consensus Avec MITTEN (démonstration)

Author

Bozman, Çagdas, Iguernlala, Mohamed, Laporte, Michael, Levillain, Maxime, Mebsout, Alain, Conchon, Sylvain, Functori, Nomadic Labs, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Chantal Keller, and Timothy Bourke

Subjects
[INFO]Computer Science [cs]
Abstract

National audience; Cet article présente Mitten, un outil pour décrire finement et jouer des scénarios sur une implémentation de Tenderbake-le prochain protocole de consensus à la pBFT de la blockchain Tezos. Mitten est paramétrable pour filtrer et examiner les messages selon des scénarios particuliers écrits dans un DSL construit sur OCaml. Grâce à Mitten, nous avons pu écrire et simuler des scénarios subtils pour reproduire des comportements difficilement atteignables en temps normal. Nous avons également pu simuler des situations permettant d'exhiber des bugs dans l'implémentation en cours et de tester des correctifs proposés.

Published
2022

44. Catala, un langage pour transformer la loi en code (démonstration)

Author

Delaët, Alain, Merigoux, Denis, École normale supérieure de Lyon (ENS de Lyon), Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Chantal Keller, Timothy Bourke, and Bourke, Timothy

Subjects
[INFO]Computer Science [cs], [INFO] Computer Science [cs]
Abstract

National audience; Le droit codifie et régit de nombreux aspects de la vie quotidienne. Si la plupart du temps les lois sont sujettes à interprétation, dans certains domaines la loi ne permet pas d'interprétation et vise essentiellement à décrire rigoureusement un calcul ou une procédure de décision, c'est-à-dire un algorithme. Catala est un nouveau langage conçu en collaboration avec des juristes qui permet une compilation depuis une spécification proche de la loi vers un code exécutable. Contrairement aux langages traditionnels, Catala est adapté aux raisonnements cas de base/exceptions présents dans la loi ; il intègre de la programmation littéraire du droit qui facilite les mises à jour du programme. Finalement, Catala compile vers une variété de langages cibles dont OCaml. Dans cette démonstration de prototype, nous montrerons comment exprimer une partie du calcul des allocations familiales dans Catala.

Published
2022

45. 33èmes Journées Francophones des Langages Applicatifs

Author

Keller, Chantal, Bourke, Timothy, Blazy, Sandrine, Bour, Frédéric, Bury, Guillaume, Dumbrava, Stefania, Gallois-Wong, Diane, Guatto, Adrien, Janin, David, Kerjean, Marie, Pellissier, Luc, Pereira, Mário, Trieu, Alix, Zakowski, Yannick, Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Parallélisme de Kahn Synchrone ( Parkas), Département d'informatique - ENS Paris (DI-ENS), École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Software certification with semantic analysis (CELTIQUE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Langages de programmation : systèmes de types, concurrence, preuve de programme (CAMBIUM), Collège de France (CdF (institution))-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Tarides [Paris], OCamlPro SAS, Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE), Nomadic Labs, Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique de Paris-Nord (LIPN), Centre National de la Recherche Scientifique (CNRS)-Université Sorbonne Paris Nord, Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Algorithmique Complexité et Logique (LACL), Université Paris-Est Créteil Val-de-Marne - Paris 12 (UPEC UP12), NOVA Laboratory for Computer Science and Informatics (NOVA-LINCS), Departamento de Informática (DI), Faculdade de Ciências e Tecnologia = School of Science & Technology (FCT NOVA), Universidade Nova de Lisboa = NOVA University Lisbon (NOVA)-Universidade Nova de Lisboa = NOVA University Lisbon (NOVA)-Faculdade de Ciências e Tecnologia = School of Science & Technology (FCT NOVA), Universidade Nova de Lisboa = NOVA University Lisbon (NOVA)-Universidade Nova de Lisboa = NOVA University Lisbon (NOVA), Aarhus University [Aarhus], Compilation et Analyse, Logiciel et Matériel (CASH), Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Lyon, Chantal Keller, Timothy Bourke, Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), and Bourke, Timothy

Subjects
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]
Abstract

International audience; Les 33èmes Journées Francophones des Langages Applicatifs (JFLA) se sont tenues à Saint-Médard-d'Excideuil, plus précisément Domaine d'Essendiéras (Périgord), du mardi 28 juin 2022 au vendredi 1er juillet 2022.Les JFLA réunissent concepteurs, utilisateurs et théoriciens ; elles ont pour ambition de couvrir les domaines des langages applicatifs, de la preuve formelle, de la vérification de programmes, et des objets mathématiques qui sous-tendent ces outils. Ces domaines doivent être pris au sens large : nous souhaitons promouvoir les ponts entre les différentes thématiques.- Langages fonctionnels et applicatifs : sémantique, compilation, optimisation, typage, mesures, extensions par d'autres paradigmes.- Assistants de preuve : implémentation, nouvelles tactiques, développements présentant un intérêt technique ou méthodologique.- Logique, correspondance de Curry-Howard, réalisabilité, extraction de programmes, modèles.- Spécification, prototypage, développements formels d'algorithmes.- Vérification de programmes ou de modèles, méthode déductive, interprétation abstraite, raffinement.- Utilisation industrielle des langages fonctionnels et applicatifs, ou des méthodes issues des preuves formelles, outils pour le web.Les articles soumis aux JFLA sont relus par au moins deux personnes s'ils sont acceptés, trois personnes s'ils sont rejetés. Les critiques des relecteurs sont toujours bienveillantes et la plupart du temps encourageantes et constructives, même en cas de rejet.

Published
2022

46. Vers une traduction de K en Dedukti

Author

Ledein, Amélie, Blot, Valentin, Dubois, Catherine, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE), Chantal Keller, and Timothy Bourke

Subjects
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], ComputingMilieux_MISCELLANEOUS
Abstract

National audience

Published
2022

47. Formalisation d'un vérificateur efficace d'assertions arithmétiques à l'exécution

Author

Benjamin, Thibaut, Ridoux, Félix, Signoles, Julien, Laboratoire Sûreté des Logiciels (LSL), Département Ingénierie Logiciels et Systèmes (DILS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay, École normale supérieure - Rennes (ENS Rennes), Bourke, Timothy, Chantal Keller, Timothy Bourke, Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA), and Financés par le programme de Recherche et Innovation Horizon2020 de l’Union Européenne sous l’accord numéro N◦ 883242, projet ENSURESEC

Subjects
[SPI.OTHER]Engineering Sciences [physics]/Other, [INFO]Computer Science [cs], [INFO] Computer Science [cs]
Abstract

International audience; La vérification d’assertions à l’exécution est une technique consistant à vérifier la validité d’annotations formelles pendant l’exécution d’un programme. Bien qu’ancienne, cette technique reste encore peu étudiée d’un point de vue théorique. Cet article contribue à pallier ce manque en formalisant un vérificateur d’assertions à l’exécution pour des propriétés arithmétiques entières. La principale difficulté réside dans la modélisation d’un générateur de code pour les propriétés visées qui génère du code à la fois correct et efficace. Ainsi, le code généré repose sur des entiers machines lorsque le générateur peut prouver qu’il est correct de le faire et sur une bibliothèque spécialisée dans l’arithmétique exacte, correcte mais moins efficace, dans les autres cas. Il utilise pour cela un système de types dédié. En outre, la logique considérée pour les propriétés inclue des constructions d’ordre supérieur. L’article présente également une implémentation de ce générateur de code au sein d’EACSL, le greffon de Frama-C dédié à la vérification d’assertions à l’exécution, ainsi qu’une première évaluation expérimentale démontrant empiriquement l’efficacité du code généré.

Published
2022

48. Certification de la transformation de tâches de preuve

Author

Garchery, Quentin, Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Université Paris-Saclay, Claude Marché, Andrei Paskevich, and Chantal Keller

Subjects
Vérification déductive de programmes, Certificates, Certificats, Deductive verification of programs, Outil de vérification déductive Why3, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Démonstration automatique, Automated reasoning, Why3 tool for deductive verification, Méthodes formelles de génie logiciel, Formal methods for software engineering
Abstract

In various provers and deductive verification tools, logical transformations are used extensively in order to reduce a proof task into a number of simpler tasks. Logical transformations are often part of the trusted base of such tools. In this thesis, we develop a framework to improve confidence in their results. We follow a skeptical} approach: transformations are instrumented to produce certificates that are checked by a third-party tool. Thus, we benefit from a modular approach that is also robust to changes in the source code of the transformations. We design two kinds of certificates. Transformations produce surface certificates} that are then translated to kernel certificates} which are destined for final verification. We made sure that surface certificates are easy to produce. Moreover, surface certificates are as independent of the transformation application as possible and this makes for a modular certification. On the contrary, kernel certificates include numerous details about the transformation application and are kept elementary. This helps to define simpler checkers and establish their correctness. We propose a translation procedure from surface certificates to kernel certificates which does not need to be trusted. Logical transformations are considered in a higher-order logic, with type polymorphism and built-in theories such as equality and integer arithmetic. We apply our framework to Why3 and use it to instrument pre-existing and complex transformations. Additionally, we implement two certificate checkers. The first one follows an efficient computational approach while the second is based on a shallow embedding of proof tasks inside the logical framework Lambdapi, thus exhibiting formal guaranties of its correctness.; De nombreux prouveurs et outils de vérification font un usage instensif des transformations logiques afin de ramener un problème exprimé sous la forme d'une tâche de preuve à un certain nombre de tâches de preuve plus simples à valider. Les transformations font souvent partie de la base de confiance de l'outil de vérification. Cette thèse a pour objectif de renforcer la confiance accordée aux transformations logiques. Les transformations sont instrumentées pour produire des certificats puis ceux-ci sont vérifiés par un outil externe: c'est l'approche sceptique. De ce fait, notre méthode est incrémentale et robuste aux modifications apportées au code des transformations. Nous définissons deux formats de certificats; les transformations génèrent des certificats de surface et ces certificats sont traduits en des certificats de noyau qui sont destinés à la vérification finale. L'accent est mis sur la facilité de production des certificats de surface et nous avons fait en sorte qu'ils soient, autant que possible, indépendants des tâches de preuve, facilitant ainsi leur composition et rendant la certification plus modulaire. Les certificats de noyau, au contraire, incluent de nombreux détails tout en restant élémentaires, de sorte que leur vérification est réalisable par un outil simple, dont la confiance est facile à établir. Nous proposons une procédure de traduction d'un certificat de surface en un certificat de noyau qui n'a pas besoin d'être certifiée. Les transformations logiques sont considérées dans une logique d'ordre supérieur avec polymorphisme de type, ce formalisme pouvant être étendu avec des théories interprétées telles que l'égalité ou l'arithmétique entière. Nous appliquons notre méthode à Why3, et notamment à des transformations complexes qui pré-existent à notre travail. Nous implémentons également deux vérificateurs de certificats, le premier reposant sur une approche calculatoire efficace et l'autre s'appuyant sur un encodage superficiel des tâches de preuve dans le framework logique Lambdapi, donnant ainsi de fortes garanties de sa correction.

Published
2022

49. Soyez prudent : prenez des photos pour l'assurance avec osnap (démonstration)

Author

Chaboche, Valentin, Dargaye, Zaynah, Jakobsson, Arvid, Bourke, Timothy, Chantal Keller, and Timothy Bourke

Subjects
[INFO] Computer Science [cs]
Abstract

Comment s'assurer que nous n'introduisons pas de bogue durant l'évolution d'un logiciel ? Les outils de snapshot testing orent une solution : le résultat d'une fonction est capturé et après modication comme de la refactorisation de code, l'outil détectera des changements. Néanmoins, le snapshot testing oblige le développeur à écrire des scénarios à la main. Nous introduisons osnap : une bibliothèque de snapshot testing avec une génération aléatoire de scénarios, d'exécution et de détection de changement de comportement inspirée par la génération aléatoire de bibliothèque comme QuickCheck en Haskell. En utilisant osnap, les développeurs peuvent sans eort générer massivement des tests de régression.

Published
2022

50. Actema : une interface graphique et gestuelle pour preuves formelles (démonstration)

Author

Donato, Pablo, Strub, Pierre-Yves, Werner, Benjamin, Bourke, Timothy, Chantal Keller, Timothy Bourke, Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion (PARTOUT), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)

Subjects
[INFO]Computer Science [cs], [INFO] Computer Science [cs], ComputingMilieux_MISCELLANEOUS
Abstract

National audience

Published
2022

Catalog

Books, media, physical & digital resources
See catalog results