Tesi: "Coq (assistant de preuve)"

1

Lelay, Catherine. "Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée". Thesis, Paris 11, 2015. http://www.theses.fr/2015PA112096/document.

Testo completo

Abstract (sommario):

L'analyse réelle a de nombreuses applications car c'est un outil approprié pour modéliser de nombreux phénomènes physiques et socio-économiques. En tant que tel, sa formalisation dans des systèmes de preuve formelle est justifié pour permettre aux utilisateurs de vérifier formellement des théorèmes mathématiques et l'exactitude de systèmes critiques. La bibliothèque standard de Coq dispose d'une axiomatisation des nombres réels et d'une bibliothèque de théorèmes d'analyse réelle. Malheureusement, cette bibliothèque souffre de nombreuses lacunes. Par exemple, les définitions des intégrales et des dérivées sont basées sur les types dépendants, ce qui les rend difficiles à utiliser dans la pratique. Cette thèse décrit d'abord l'état de l'art des différentes bibliothèques d'analyse réelle disponibles dans les assistants de preuve. Pour pallier les insuffisances de la bibliothèque standard de Coq, nous avons conçu une bibliothèque facile à utiliser : Coquelicot. Une façon plus facile d'écrire les formules et les théorèmes a été mise en place en utilisant des fonctions totales à la place des types dépendants pour écrire les limites, dérivées, intégrales et séries entières. Pour faciliter l'utilisation, la bibliothèque dispose d'un ensemble complet de théorèmes couvrant ces notions, mais aussi quelques extensions comme les intégrales à paramètres et les comportements asymptotiques. En plus, une hiérarchie algébrique permet d'appliquer certains théorèmes dans un cadre plus générique comme les nombres complexes pour les matrices. Coquelicot est une extension conservative de l'analyse classique de la bibliothèque standard de Coq et nous avons démontré les théorèmes de correspondance entre les deux formalisations. Nous avons testé la bibliothèque sur plusieurs cas d'utilisation : sur une épreuve du Baccalauréat, pour les définitions et les propriétés des fonctions de Bessel ainsi que pour la solution de l'équation des ondes en dimension 1
Real analysis is pervasive to many applications, if only because it is a suitable tool for modeling physical or socio-economical systems. As such, its support is warranted in proof assistants, so that the users have a way to formally verify mathematical theorems and correctness of critical systems. The Coq system comes with an axiomatization of standard real numbers and a library of theorems on real analysis. Unfortunately, this standard library is lacking some widely used results. For instance, the definitions of integrals and derivatives are based on dependent types, which make them cumbersome to use in practice. This thesis first describes various state-of-the-art libraries available in proof assistants. To palliate the inadequacies of the Coq standard library, we have designed a user-friendly formalization of real analysis: Coquelicot. An easier way of writing formulas and theorem statements is achieved by relying on total functions in place of dependent types for limits, derivatives, integrals, power series, and so on. To help with the proof process, the library comes with a comprehensive set of theorems that cover not only these notions, but also some extensions such as parametric integrals and asymptotic behaviors. Moreover, an algebraic hierarchy makes it possible to apply some of the theorems in a more generic setting, such as complex numbers or matrices. Coquelicot is a conservative extension of the classical analysis of Coq's standard library and we provide correspondence theorems between the two formalizations. We have exercised the library on several use cases: in an exam at university entry level, for the definitions and properties of Bessel functions, and for the solution of the one-dimensional wave equation

Gli stili APA, Harvard, Vancouver, ISO e altri

2

Sall, Boubacar Demba. "Programmation impérative par raffinements avec l'assistant de preuve Coq". Electronic Thesis or Diss., Sorbonne université, 2020. http://www.theses.fr/2020SORUS181.

Testo completo

Abstract (sommario):

Cette thèse s’intéresse à la programmation certifiée correcte dans le cadre formel fourni par l’assistant de preuve Coq, et conduite par étapes de raffinements, avec l'objectif d’aboutir à un résultat correct par construction. Le langage de programmation considéré est un langage impératif simple, avec affectations, alternatives, séquences, et boucles. La sémantique associée à ce langage est une sémantique relationnelle exprimée dans un cadre prédicatif plus adapté à un plongement dans la théorie des types, plutôt que dans le calcul des relations. Nous étudions la relation entre d’une part la sémantique prédicative et relationnelle que nous avons choisie, et d’autre part une approche plus classique dans le style de la logique de Hoare. En particulier, nous montrons que les deux approches ont en théorie la même puissance. La démarche que nous étudions consiste à certifier, avec l’aide d’un assistant de preuve, les raffinements successifs permettant de passer de la spécification au programme. Nous nous intéressons donc aussi aux techniques de preuve permettant en pratique d’établir la validité des raffinements. Plus précisément, nous utilisons un calcul de la plus faible pré-spécification jouant ici le rôle du calcul de la plus faible pré-condition dans les approches classiques. Afin que l’articulation des étapes de raffinement reste aussi proche que possible de l’activité de programmation, nous formalisons un langage de développement qui permet de décrire l’arborescence des étapes de raffinement, ainsi qu’une logique permettant de raisonner sur ces développements, et de garantir leur correction
This thesis investigates certified programming by stepwise refinement in the framework of the Coq proof assistant. This allows the construction of programs that are correct by construction. The programming language that is considered is a simple imperative language with assignment, selection, sequence, and iteration. The semantics of this language is formalized in a relational and predicative setting, and is shown to be equivalent to an axiomatic semantics in the style of a Hoare logic. The stepwise refinement approach to programming requires that refinement steps from the specification to the program be proved correct. For so doing, we use a calculus of weakest pre-specifications which is a generalisation of the calculus of weakest pre-conditions. Finally, to capture the whole refinement history of a program development, we formalize a design language and a logic for reasoning about program designs in order to establish that all refinement steps are indeed correct. The approach developed during this thesis is entirely mecanised using the Coq proof assistant

Gli stili APA, Harvard, Vancouver, ISO e altri

3

Filou, Vincent. "Une étude formelle de la théorie des calculs locaux à l'aide de l'assistant de preuve Coq". Thesis, Bordeaux 1, 2012. http://www.theses.fr/2012BOR14708/document.

Testo completo

Abstract (sommario):

L'objectif de cette thèse est de produire un environnement permettant de raisonner formellement sur la correction de systèmes de calculs locaux, ainsi que sur l'expressivité de ce modèle de calcul. Pour ce faire, nous utilisons l'assistant de preuve Coq. Notre première contribution est la formalisation en Coq de la sémantique des systèmes de réétiquetage localement engendrés, ou calculs locaux. Un système de calculs locaux est un système de réétiquetage de graphe dont la portée est limitée. Nous proposons donc tout d'abord une implantation succincte de la théorie des graphes en Coq, et utilisons cette dernière pour définir les systèmes de réétiquetage de graphes localement engendrés. Nous avons relevé, dans la définition usuelle des calculs locaux, certaines ambiguïtés. Nous proposons donc une nouvelle définition, et montrons formellement que celle-ci capture toutes les sous-classes d'algorithmes étudiées. Nous esquissons enfin une méthodologie de preuve des systèmes de calculs locaux en Coq.Notre seconde contribution consiste en l'étude formelle de l'expressivité des systèmes de calculs locaux. Nous formalisons un résultat de D. Angluin (repris par la suite par Y. Métivier et J. Chalopin): l'inexistence d'un algorithme d'élection universelle. Nous proposons ensuite deux lemmes originaux concernant les calculs locaux sur les arêtes (ou systèmes LC0), et utilisons ceux-ci pour produire des preuves formelles d'impossibilité pour plusieurs problèmes: calcul du degré de chaque sommet, calcul d'arbre recouvrant, etélection. Nous proposons informellement une nouvelles classes de graphe pour laquelle l'élection est irréalisable par des calculs locaux sur les arêtes.Nous étudions ensuite les transformations de systèmes de calculs locaux et de leur preuves. Nous adaptons le concept de Forward Simulation de N. Lynch aux systèmes de calculs locaux et utilisons ce dernier pour démontrer formellement l'inclusion de deux modes de détection de terminaison dans le cas des systèmes LC0. La preuve de cette inclusion estsimplifiée par l'utilisation de transformations "standards" de systèmes, pour lesquels des résultats génériques ont été démontrés. Finalement, nous réutilisons ces transformations standards pour étudier, en collaboration avec M. Tounsi, deux techniques de composition des systèmes de réétiquetage LC0. Une bibliothèque Coq d'environ 50000 lignes, contenant les preuves formelles des théorèmes présentés dans le mémoire de thèse à été produite en collaboration avec Pierre Castéran (dont environ 40%produit en propre par V. Filou) au cours de cette thèse
The goal of this work is to build a framework allowing the study, in aformal setting, of the correctness of local computations systems aswell as the expressivity of this model. A local computation system isa set of graph relabelling rules with limited scope, corresponding to a class of distributed algorithms.Our first contribution is the formalisation, in the Coq proofassistant, of a relationnal semantic for local computation systems.This work is based on an original formal graph theory for Coq.Ambiguities inherent to a "pen and paper" definition of local computations are corrected, and we prove that our definition captures all sub-classes of relabelling relations studied in the remainder. We propose a draft of a proof methodology for local computation systems in Coq. Our second contribution is the study of the expressivity of classes of local computations inside our framework. We provide,for instance, a formal proof of D. Angluin results on election and graph coverings. We propose original "meta-theorems" concerningthe LC0 class of local computation, and use these theorem to produce formal impossibility proofs.Finally we study possible transformations of local computation systemsand of their proofs. To this end, we adapt the notion of ForwardSimulation, originally formulated by N. Lynch, to localcomputations. We use this notion to define certified transformationsof LC0 systems. We show how those certified transformation can be useto study the expressivity of certain class of algorithm in ourframework. We define, as certified transformation, two notions ofcomposition for LC0 systems.A Coq library of ~ 50000 lines of code, containing the formal proofs of the theorems presented in the thesis has been produced in collaboration with Pierre Castéran

Gli stili APA, Harvard, Vancouver, ISO e altri

4

Zucchini, Rébecca. "Bibliothèque certifiée en Coq pour la provenance des données". Electronic Thesis or Diss., université Paris-Saclay, 2023. http://www.theses.fr/2023UPASG040.

Testo completo

Abstract (sommario):

La présente thèse se situe à l'intersection des méthodes formelles et des bases de données, et s'intéresse à la formalisation de la provenance des données à l'aide de l'assistant de preuve Coq. L'étude de la provenance des données, qui permet de retracer leur origine et leur historique, est essentielle pour assurer la qualité des données, éviter les interprétations erronées et favoriser la transparence dans le traitement des données. La thèse propose ainsi la formalisation de deux types de provenance des données couramment utilisés, la How-provenance et la Where-provenance. Cette formalisation a permis de comparer leur sémantique, mettant en évidence leurs différences et leurs complémentarités. En outre, elle a conduit à la proposition d'une structure algébrique et d'une sémantique unificatrice pour ces deux types de provenance
This thesis is about the formalization of data provenance using the Coq proof assistant, at the intersection of formal methods and database communities. It explores the importance of data provenance, which tracks the origin and history of data, in addressing issues such as poor data quality, incorrect interpretations, and lack of transparency in data processing. The thesis proposes formalizations of two commonly used types of data provenance, How-provenance and Where-provenance. Formalizing both types of provenance allowed us to compare their semantics, highlighting their differences and complementarities. Additionally, the formalization of these two types of provenance led to the proposal of an algebraic structure that provides a unifying semantics

Gli stili APA, Harvard, Vancouver, ISO e altri

5

Braun, David. "Approche combinatoire pour l'automatisation en Coq des preuves formelles en géométrie d'incidence projective". Thesis, Strasbourg, 2019. http://www.theses.fr/2019STRAD020.

Testo completo

Abstract (sommario):

Ce travail de thèse s’inscrit dans le domaine de la preuve assistée par ordinateur et se place d'un point de vue méthodologique. L’objectif premier des assistants de preuves est de vérifier qu’une preuve écrite à la main est correcte; la question ici est de savoir comment à l’intérieur d’un tel système, il est possible d'aider un utilisateur à fabriquer une preuve formelle du résultat auquel il s'intéresse. Ces questions autour de la vérification de preuves, en particulier en certification du logiciel, et au delà de leur traçabilité et de leur lisibilité sont en effet devenues prégnantes avec l’importance qu’ont prise les algorithmes dans notre société. Bien évidemment, répondre à la question de l’aide à la preuve dans toute sa généralité dépasse largement le cadre de cette thèse. C’est pourquoi nous focalisons nos travaux sur la preuve en mathématiques dans un cadre particulier qui est bien connu dans notre équipe : la géométrie et sa formalisation dans le système Coq. Dans ce domaine, nous mettons premièrement en évidence les niveaux auxquels on peut oeuvrer à savoir le contexte scientifique à travers les méthodes de formalisation mais aussi le contexte méthodologique et technique au sein de l'assistant de preuve Coq. Dans un second temps, nous essayons de montrer comment nos méthodes et nos idées sont généralisables à d'autres disciplines. Nous mettons ainsi en place dans nos travaux les premiers jalons pour une aide à la preuve efficace dans un contexte géométrique simple mais omniprésent. À travers une approche classique fondée sur la géométrie synthétique et une approche combinatoire complémentaire utilisant le concept de rang issu de la théorie des matroïdes, nous fournissons à l'utilisateur des principes généraux et des outils facilitant l'élaboration de preuves formelles. Dans ce sens, nous comparons les capacités d'automatisation de ces deux approches dans le contexte précis des géométries finies avant de finalement construire un prouveur automatique de configuration géométrique d'incidence
This thesis work is part of the general field of computer-assisted proof and is methodologically based. The primary objective of proof assistants is to verify that handwritten demonstration is correct; the question here is how within such a system, it is possible to help a user to make a formal proof of the result in which he is interested. These questions around the verification of proofs, in particular in software certification, and beyond their traceability and readability have indeed become significant with the importance that algorithms have taken on in our society. Obviously, answering the question of proof assistance in all its generality goes far beyond the scope of this thesis. This is why we focus our work on proof in mathematics in a particular framework that is well known in our team: geometry and its formalization in the Coq system. In this field, we first highlight the levels at which we can work, namely the scientific context through the formalization methods but also the methodological and technical context within the Coq proof assistant. In a second step, we try to show how our methods and ideas can be generalized to other disciplines. In this way, we are putting in place the first steps towards effective proof assistance in a simple but omnipresent geometric context. Through a classical approach based on synthetic geometry and a complementary combinatorial approach using the concept of rank from matroid theory, we provide the user with general principles and tools to facilitate the development of formal proof. In this sense, we compare the automation capabilities of these two approaches in the specific context of finite geometries before finally constructing an automatic prover of geometric configurations of incidence

Gli stili APA, Harvard, Vancouver, ISO e altri

6

Mouhcine, Houda. "Formal Proofs in Applied Mathematics : A Coq Formalization of Simplicial Lagrange Finite Elements". Electronic Thesis or Diss., université Paris-Saclay, 2024. https://theses.hal.science/tel-04884651.

Testo completo

Abstract (sommario):

Cette thèse est dédiée au développement de preuves formelles de théorèmes et propositions mathématiques dans le domaine de l'analyse réelle, en utilisant l'assistant de preuve Coq pour garantir leur exactitude. Le cœur de ce travail est divisé en deux parties principales.La première partie se concentre sur l'utilisation de Coq pour formaliser des principes mathématiques clés tels que le principe d'induction de Lebesgue et le théorème de Tonelli, permettant le calcul d'intégrales doubles sur des espaces produits en intégrant de manière itérative par rapport à chaque variable. Ce travail s'appuie sur des recherches antérieures en théorie de la mesure et sur l'intégrale de Lebesgue.La deuxième partie de cette thèse fonctionne dans le cadre de la méthode des éléments finis (MEF), une technique numérique largement utilisée pour résoudre des équations aux dérivées partielles (EDP). La MEF joue un rôle important dans de nombreux programmes de simulation industrielle, notamment dans l'approximation des solutions à des problèmes complexes tels que le transfert de chaleur, la dynamique des fluides et les simulations de champs électromagnétiques. Plus spécifiquement, nous visons à construire des éléments finis, en nous concentrant sur les éléments finis de Lagrange simpliciaux avec des degrés de liberté répartis uniformément. Ce travail mobilise un large éventail de concepts algébriques, y compris les familles finies, les monoïdes, les espaces vectoriels, les espaces affines, les sous-structures et les espaces de dimensions finies.Pour mener à bien cette étude, nous formalisons dans Coq en logique classique plusieurs composants fondamentaux. Nous commençons par construire un élément fini général, puis nous procédons à la définition de plusieurs composants fondamentaux, y compris la construction de l'espace d'approximation de Lagrange, l'expression de sa base de polynômes de Lagrange et la formalisation des transformations géométriques affines et de la propriété d'unisolvance des éléments finis de Lagrange
This thesis is dedicated to developing formal proofs of mathematical theorems and propositions within the field of real analysis using the Coq proof assistant to ensure their correctness. The core of this work is divided into two main parts.The first part focuses on using Coq to formalize key mathematical principles such as the Lebesgue induction principle and the Tonelli theorem, allowing the computation of double integrals on product spaces by iteratively integrating with respect to each variable. This work builds upon previous research in measure theory and the Lebesgue integral.The second part of this thesis operates within the framework of the Finite Element Method (FEM), a widely used numerical technique for solving partial differential equations (PDEs). FEM plays an important role in numerous industrial simulation programs, particularly in approximating solutions to complex problems such as heat transfer, fluid dynamics, and electromagnetic field simulations. Specifically, we aim to construct finite elements, focusing on simplicial Lagrange finite elements with evenly distributed degrees of freedom. This work engages a broad range of algebraic concepts, including finite families, monoids, vector spaces, affine spaces, substructures, and finite-dimensional spaces.To conduct this study, we formalize in Coq in classical logic several foundational components. We begin by constructing a general finite element, then proceed to define several foundational components, including the construction of the Lagrange approximation space, expressing its Lagrange polynomial basis, and formalizing affine geometric transformations and the unisolvence property of Lagrange finite elements

Gli stili APA, Harvard, Vancouver, ISO e altri

7

Dubois, De Prisque Louise. "Prétraitement compositionnel en Coq". Electronic Thesis or Diss., université Paris-Saclay, 2024. http://www.theses.fr/2024UPASG040.

Testo completo

Abstract (sommario):

Cette thèse présente une méthodologie de prétraitement visant à transformer certains énoncés de la logique de l'assistant de preuve Coq en énoncés de logique du premier ordre, de façon à les envoyer à des prouveurs automatiques, et en particulier des prouveurs SMT. Cette méthodologie consiste à composer de petites transformations indépendantes et certifiantes, prenant la forme de tactiques Coq. Une implémentation de cette méthodologie est proposée dans un plugin appelé Sniper, qui offre une tactique "pousse-bouton" d'automatisation. Par ailleurs, un ordonnanceur de transformations logiques permet d'ajouter ses propres transformations logiques à l'ensemble et de déterminer quelles transformations s'appliquent en fonction de la preuve à effectuer
This thesis presents a preprocessing methodology aimed at transforming certain statements from the Coq proof assistant's logic into first-order logic statements, in order to send them to automatic provers, in particular SMT solvers. This methodology involves composing small, independent, and certifying transformations, taking the form of Coq tactics. An implementation of this methodology is provided in a plugin called Sniper, which offers a "push-button" automation tactic. Furthermore, a logical transformation scheduler (called Orchestrator) allows adding one's own logical transformations and determines which transformations apply depending on the proof to be carried out

Gli stili APA, Harvard, Vancouver, ISO e altri

8

Keller, Chantal. "A Matter of Trust : Skeptical Communication between Coq and External Provers". Palaiseau, Ecole polytechnique, 2013. http://pastel.archives-ouvertes.fr/docs/00/83/83/22/PDF/thesis-keller.pdf.

Testo completo

Abstract (sommario):

Cette thèse présente une coopération entre l'assistant de preuve Coq et certains prouveurs externes basée sur l'utilisation de traces de preuves. Nous étudions plus particulièrement deux types de prouveurs pouvant renvoyer des certicats : d'une part, les réponses des prouveurs SAT et SMT peuvent être vériées en Coq afin d'augmenter à la fois la confiance qu'on peut leur porter et l'automatisation de Coq ; d'autre part, les théorèmes établis dans des assistants de preuves basés sur la Logique d'Ordre Supérieur peuvent être exportés en Coq et re-vérifiés, ce qui permet d'établir des preuves formelles mêlant ces deux paradigmes logiques. Cette étude a abouti à deux logiciels : SMTCoq, une coopération bi-directionnelle entre Coq et des prouveurs SAT/SMT, et HOLLIGHTCOQ, un outil important les théorèmes de HOL Light en Coq. L'architecture de chacun de ces deux développements a été pensée de manière modulaire et efficace, en établissant une séparation claire entre trois composants: un encodage en Coq du formalisme de l'outil externe qui est ensuite traduit avec soin vers des termes Coq, un vérificateur certifié pour établir les preuves, et un pré-processeur écrit en Ocaml traduisant les traces venant de prouveurs différents dans le même format de certicat. Grâce à cette séparation, un changement dans le format de traces n'affecte que le pré-processeur, sans qu'il soit besoin de modier du code ou des preuves Coq. Un autre composant essentiel pour l'efficacité et la modularité est la réflexion calculatoire, qui utilise les capacités de calcul de Coq pour établir des preuves à la fois courtes et génériques à partir des certificats
This thesis studies the cooperation between the Coq proof assistant and external provers through proof witnesses. We concentrate on two different kinds of provers that can return certicates: first, answers coming from SAT and SMT solvers can be checked in Coq to increase both the confidence in these solvers and Coq's automation; second, theorems established in interactive provers based on Higher-Order Logic can be exported to Coq and checked again, in order to offer the possibility to produce formal developments which mix these two dierent logical paradigms. It ended up in two software: SMTCoq, a bi-directional cooperation between Coq and SAT/SMT solvers, and HOLLIGHTCOQ, a tool importing HOL Light theorems into Coq. For both tools, we took great care to define a modular and efficient architecture, based on three clearly separated ingredients: an embedding of the formalism of the external tool inside Coq which is carefully translated into Coq terms, a certified checker to establish the proofs using the certicates, and an Ocaml preprocessor to transform proof witnesses coming from different provers into a generic certificate. This division allows that a change in the format of proof witnesses only affects the preprocessor, but no proved Coq code. Another fundamental component for efficiency and modularity is computational reflection, which exploits the computational power of Coq to establish generic and small proofs based on the certicates

Gli stili APA, Harvard, Vancouver, ISO e altri

9

Paulin-Mohring, Christine. "Définitions Inductives en Théorie des Types". Habilitation à diriger des recherches, Université Claude Bernard - Lyon I, 1996. http://tel.archives-ouvertes.fr/tel-00431817.

Testo completo

Abstract (sommario):

Ce document donne un panorama de la représentation des définitions inductives dans différents assistants de preuve en logique d'ordre supérieur, théorie des ensembles et théorie des types. Il présente, étudie et justifie les choix faits dans le système Coq.

Gli stili APA, Harvard, Vancouver, ISO e altri

10

Herms, Paolo. "Certification of a Tool Chain for Deductive Program Verification". Phd thesis, Université Paris Sud - Paris XI, 2013. http://tel.archives-ouvertes.fr/tel-00789543.

Testo completo

Abstract (sommario):

This thesis belongs to the domain of software verification. The goalof verifying software is to ensure that an implementation, a program,satisfies the requirements, the specification. This is especiallyimportant for critical computer programs, such as control systems forair planes, trains and power plants. Here a malfunctioning occurringduring operation would have catastrophic consequences. Software requirements can concern safety or functioning. Safetyrequirements, such as not accessing memory locations outside validbounds, are often implicit, in the sense that any implementation isexpected to be safe. On the other hand, functional requirementsspecify what the program is supposed to do. The specification of aprogram is often expressed informally by describing in English or someother natural language the mission of a part of the program code.Usually program verification is then done by manual code review,simulation and extensive testing. But this does not guarantee that allpossible execution cases are captured. Deductive program proving is a complete way to ensure soundness of theprogram. Here a program along with its specificationis a mathematical object and its desired properties are logicaltheorems to be formally proved. This way, if the underlying logicsystem is consistent, we can be absolutely sure that the provenproperty holds for the program in any case.Generation of verification conditions is a technique helpingthe programmer to prove the properties he wants about his programs.Here a VCG tool analyses a program and its formal specification andproduces a mathematical formula, whose validity implies the soundnessof the program with respect to its specification. This is particularlyinteresting when the generated formulas can be proved automatically byexternal SMT solvers.This approach is based on works of Hoare and Dijkstra and iswell-understood and shown correct in theory. Deductive verificationtools have nowadays reached a maturity allowing them to be used inindustrial context where a very high level of assurance isrequired. But implementations of this approach must deal with allkinds of language features and can therefore become quite complex andcontain errors -- in the worst case stating that a program correcteven if it is not. This raises the question of the level ofconfidence granted to these tools themselves. The aim of this thesis is to address this question. We develop, inthe Coq system, a certified verification-condition generator (VCG) forACSL-annotated C programs.Our first contribution is the formalisation of an executableVCG for the Whycert intermediate language,an imperative language with loops, exceptions and recursive functionsand its soundness proof with respect to the blocking big-step operational semantics of the language.A second contribution is the formalisation of the ACSL logicallanguage and the semantics of ACSL annotations of Compcert's Clight.From the compilation of ACSL annotated Clight programs to Whycertprograms and its semantics preservation proof combined with a Whycertaxiomatisation of the Compcert memory model results our maincontribution: an integrated certified tool chainfor verification of C~programs on top of Compcert. By combining oursoundness result with the soundness of the Compcert compiler we obtaina Coq theorem relating the validity of the generated proof obligationswith the safety of the compiled assembly code.

Gli stili APA, Harvard, Vancouver, ISO e altri

11

Nigron, Pierre. "Effectful programs and their proofs in type theory : application to certified compilation and certified packet processing". Electronic Thesis or Diss., Sorbonne université, 2022. http://www.theses.fr/2022SORUS480.

Testo completo

Abstract (sommario):

Pour pouvoir raisonner sur nos programmes, une méthode est de directement les écrire dans un assistant de preuve. Utilisant la correspondance de Curry-Howard, les programmes et les preuves ne font alors qu’un. Pour ne pas nuire à la cohérence logique de l’assistant de preuve, le système est obligé de restreindre les programmes à ne pas avoir d’effets de bord. Cependant, les effets de bord sont omniprésents et essentiels dans la programmation. Différentes techniques telles que les monades ou les effets algébriques ont alors émergé pour les modéliser offrant ainsi un moyen d'écrire des programmes impératifs dans des langages purement fonctionnels. C'est donc assez naturellement que les résultats de décennies de recherches investies pour raisonner sur des programmes impératifs tentent d'être adaptés au raisonnement sur des programmes avec effets. Dans cette thèse, nous nous intéressons d'abord à l'utilisation de la logique de séparation pour raisonner sur des programmes avec effets implémentés dans un assistant de preuve. Nous étudions une approche consistant à décrire les comportements des effets à l'aide d'un transformateur de prédicats. Nous nous concentrons d'abord sur la fraîcheur, puis sur le traitement de paquets et le zéro-copie. Pour étudier notre approche, nous nous appuyons sur deux exemples concrets qui sont le module SimplExpr de CompCert et la bibliothèque de décodeur Nom. Pour finir, pour compiler les analyseurs de paquets produits vers C, nous proposons une méthode par raffinement supprimant les continuations introduites par l'utilisation d'une monade libre et effectuant quelques optimisations
One way to reason about our programs is to write them directly into a proof assistant. Using the Curry-Howard correspondence, programs and proofs are then one. In order not to undermine the logical consistency of the proof assistant, the system is forced to restrict the programs to have no side effects. However, side effects are ubiquitous and essential in programming. Different techniques such as monads or algebraic effects have emerged to model them, thus offering a way to write imperative programs in purely functional languages. It is therefore quite natural that the results of decades of research invested in reasoning about imperative programs try to be adapted to reasoning about programs with effects. In this thesis, we are first interested in the use of separation logic to reason about programs with effects implemented in a proof assistant. We study an approach to describe the behaviour of effects using a predicate transformer. We focus first on freshness, then on packet processing and zero-copy. To study our approach, we rely on two concrete examples which are the SimplExpr module of CompCert and the decoder library Nom. Finally, in order to compile the packet parsers produced to C, we propose a refinement method removing the continuations introduced by the use of a free monad and performing some optimizations

Gli stili APA, Harvard, Vancouver, ISO e altri

12

Colin, Samuel. "Contribution à l'intégration de temporalité au formalisme B : Utilisation du calcul des durées en tant que sémantique temporelle pour B". Phd thesis, Université de Valenciennes et du Hainaut-Cambresis, 2006. http://tel.archives-ouvertes.fr/tel-00123899.

Testo completo

Abstract (sommario):

Dans le domaine des systèmes informatisés où la fiabilité est la première priorité, les méthodes formelles ont prouvé leur efficacité pour la conception de logiciels sûrs. La dépendance à de tels systèmes augmente, et les contraintes rencontrées se font plus diverses et précises, en particulier les contraintes temporelles. Certaines méthodes formelles, notamment la méthode B, rendent la conception malaisée sous de telles contraintes, puisqu'elles n'ont pas été prévues pour cela à l'origine.

Nous nous proposons donc d'étendre la méthode B pour lui permettre de spécifier et valider des systèmes à contraintes temporelles complexes. Nous utilisons pour ce faire des calculs de durées pour exprimer la sémantique du langage B et en déduire une extension conservative qui permet de l'utiliser à la fois dans son cadre d'origine et dans le cadre de systèmes à contraintes temporelles.

Nous nous penchons également sur le problème de l'utilisation d'un outil de preuve générique pour valider des formules de calcul des durées. La généricité de ce type d'outil répond à la multiplication des méthodes formelles, mais pose le problème de l'intégration des fondations mathématiques de ces méthodes à un outil générique. Nous proposons donc d'étudier la mise en oeuvre en plongement léger du calcul des durées dans l'assistant de preuve Coq. Nous en déduisons un retour sur expérience de la définition d'une logique modale particulière dans un outil à vocation générique.

Gli stili APA, Harvard, Vancouver, ISO e altri

13

Boutillier, Pierre. "De nouveaux outils pour calculer avec des inductifs en Coq". Phd thesis, Université Paris-Diderot - Paris VII, 2014. http://tel.archives-ouvertes.fr/tel-01054723.

Testo completo

Abstract (sommario):

En ajoutant au lambda-calcul des structures de données algébriques, des types dépendants et un système de modules, on obtient un langage de programmation avec peu de primitives mais une très grande expressivité. L'assistant de preuve Coq s'appuie sur un tel langage (le CIC) à la sémantique particulièrement claire. L'utilisateur n'écrit pas directement de programme en CIC car cela est ardu et fastidieux. Coq propose un environnement de programmation qui facilite la tâche en permettant d'écrire des programmes incrémentalement grâce à des constructions de haut niveau plus concises. Typiquement, les types dépendants imposent des contraintes fortes sur les données. Une analyse de cas peut n'avoir à traiter qu'un sous-ensemble des constructeurs d'un type algébrique, les autres étant impossibles par typage. Le type attendu dans chacun des cas varie en fonction du constructeur considéré. L'impossibilité de cas et les transformations de type doivent être explicitement écrites dans les termes de Coq. Pourtant, ce traitement est mécanisable et cette thèse décrit un algorithme pour réaliser cette automatisation. Par ailleurs, il est nécessaire à l'interaction avec l'utilisateur de calculer des programmes du CIC sans faire exploser la taille syntaxique de la forme réduite. Cette thèse présente une machine abstraite conçu dans ce but. Enfin, les points fixes permettent une manipulation aisée des structure de données récursives. En contrepartie, il faut s'assurer que leur exécution termine systématiquement. Cette question sensible fait l'objet du dernier chapitre de cette thèse.

Gli stili APA, Harvard, Vancouver, ISO e altri

14

Izerrouken, Nassima. "Développement prouvé de composants formels pour un générateur de code embarqué critique pré-qualifié". Thesis, Toulouse, INPT, 2011. http://www.theses.fr/2011INPT0137/document.

Testo completo

Abstract (sommario):

Nous nous intéressons au développement prouvé de composants formels pour un générateur de code pré-qualifié. Ce dernier produit un code séquentiel (C et Ada) pour des modèles d'entrée qui combinent les flots de données et de contrôle et qui présentent des possibilités d'exécution concurrente (Simulink/Stateflow et Scicos). Le développement prouvé permet de réduire le coût des tests et d'augmenter l'assurance des outils développés avec cette approche vis-à-vis de la qualification. Les phases de spécification, de développement et de vérification des outils développés sont effectuées avec l'assistant de preuve Coq. Ce dernier permet d'extraire le contenu calculatoire des composants en préservant les propriétés prouvées en Coq. Ce code extrait est ensuite intégré dans une chaîne complète de développement (chaîne de GeneAuto). Nous présentons un cadre formel, inspiré de l'analyse statique, qui s'appuie sur la sémantique abstraite et qui est instanciable sur plusieurs composants du générateur de code. Nous nous basons sur les ensembles partiellement ordonnés et sur le calcul de point fixe pour définir le cadre et effectuer les différentes analyses des composants du générateur de code. Ce cadre formel comporte toutes les preuves communes aux composants et indépendantes des analyses effectuées. Deux composants sont étudiés : l'ordonnanceur et le typeur des modèles d'entrée
We are interested in the proved development of formal components for a pre-qualified code generator. This produces a sequential code (C and Ada) for input models that combine data and control flows, with potential concurrent execution (Simulink/Stateflow and Scicos). The proved development reduces test cost and increases insurance of components developed with this approach regarding the qualification. Phases of specification, development and verification of the developed components are done with the Coq proof assistant. This allows to extract the computational content of the components preserving the properties proved in Coq. The extracted code is then integrated into the complete development tool-chain (GeneAuto tool-chain). We present a formal framework, inspired from static analysis, based on the abstract semantics which is instantiable to several components of the code generator. We rely on partially ordered sets and fixed-point to define de formal framework and to perform the various analysis of components of the code generator. This formal framework includes all proofs common to the components and independent from the performed analyses. Two components are studied : the scheduler and the type checker of input models

Gli stili APA, Harvard, Vancouver, ISO e altri

15

Keller, Chantal. "Question de confiance : communication sceptique entre Coq et des prouveurs externes". Phd thesis, Ecole Polytechnique X, 2013. http://pastel.archives-ouvertes.fr/pastel-00838322.

Testo completo

Abstract (sommario):

Cette thèse présente une coopération entre l'assistant de preuve Coq et certains prouveurs externes basée sur l'utilisation de traces de preuves. Nous étudions plus particulièrement deux types de prouveurs pouvant renvoyer des certicats : d'une part, les réponses des prouveurs SAT et SMT peuvent être vériées en Coq afin d'augmenter à la fois la confiance qu'on peut leur porter et l'automatisation de Coq ; d'autre part, les théorèmes établis dans des assistants de preuves basés sur la Logique d'Ordre Supérieur peuvent être exportés en Coq et re-vérifiés, ce qui permet d'établir des preuves formelles mêlant ces deux paradigmes logiques. Cette étude a abouti à deux logiciels : SMTCoq, une coopération bi-directionnelle entre Coq et des prouveurs SAT/SMT, et HOLLIGHTCOQ, un outil important les théorèmes de HOL Light en Coq. L'architecture de chacun de ces deux développements a été pensée de manière modulaire et efficace, en établissant une séparation claire entre trois composants: un encodage en Coq du formalisme de l'outil externe qui est ensuite traduit avec soin vers des termes Coq, un vérificateur certifié pour établir les preuves, et un pré-processeur écrit en Ocaml traduisant les traces venant de prouveurs différents dans le même format de certicat. Grâce à cette séparation, un changement dans le format de traces n'affecte que le pré-processeur, sans qu'il soit besoin de modier du code ou des preuves Coq. Un autre composant essentiel pour l'efficacité et la modularité est la réflexion calculatoire, qui utilise les capacités de calcul de Coq pour établir des preuves à la fois courtes et génériques à partir des certificats.

Gli stili APA, Harvard, Vancouver, ISO e altri

16

Zanella, Beguelin Santiago. "Certification formelle de preuves cryptographiques basées sur les séquences de jeux". Phd thesis, École Nationale Supérieure des Mines de Paris, 2010. http://pastel.archives-ouvertes.fr/pastel-00584350.

Testo completo

Abstract (sommario):

Les séquences de jeux sont une méthodologie établie pour structurer les preuves cryptographiques. De telles preuves peuvent être formalisées rigoureusement en regardant les jeux comme des programmes probabilistes et en utilisant des méthodes de vérification de programmes. Cette thèse décrit CertiCrypt, un outil permettant la construction et vérification automatique de preuves basées sur les jeux. CertiCrypt est implémenté dans l'assistant à la preuve Coq, et repose sur de nombreux domaines, en particulier les probabilités, la complexité, l'algèbre, et la sémantique des langages de programmation. CertiCrypt fournit des outils certifiés pour raisonner sur l'équivalence de programmes probabilistes, en particulier une logique de Hoare relationnelle, une théorie équationnelle pour l'équivalence observationnelle, une bibliothèque de transformations de programme, et des techniques propres aux preuves cryptographiques, permettant de raisonner sur les évènements. Nous validons l'outil en formalisant les preuves de sécurité de plusieurs exemples emblématiques, notamment le schéma de chiffrement OAEP et le schéma de signature FDH.

Gli stili APA, Harvard, Vancouver, ISO e altri

17

Jourdan, Jacques-Henri. "Verasco : a Formally Verified C Static Analyzer". Sorbonne Paris Cité, 2016. http://www.theses.fr/2016USPCC021.

Testo completo

Abstract (sommario):

Afin de développer des logiciels plus sûrs pour des applications critiques, certains analyseurs statiques tentent d'établir, avec une certitude mathématique, l'absence de certains types de bugs dans un programme donné. Une limite possible à cette approche est l'éventualité d'un bug affectant la correction de l'analyseur lui-même, éliminant ainsi les garanties qu'il est censé apporter. Dans cette thèse, nous proposons d'établir des garanties formelles sur l'analyseur lui-même : nous présentons la conception, l'implantation et la preuve de sûreté en Coq de Verasco, un analyseur statique formellement vérifié utilisant l'interprétation abstraite pour le langage ISO C99 avec l'arithmétique flottante IEEE754 (à l'exception de la récursion et de l'allocation dynamique de mémoire). Verasco a pour but d'établir l'absence d'erreur à l'exécution des programmes donnés. Il est conçu selon une architecture modulaire et extensible contenant plusieurs domaines abstraits et des interfaces bien spécifiées. Nous détaillons le fonctionnement de l'itérateur abstrait de Verasco, son traitement des entiers bornés de la machine, son domaine abstrait d'intervalles, son domaine abstrait symbolique et son domaine abstrait d'octogones. Verasco a donné lieu au développement de nouvelles techniques pour implémenter des structures de données avec partage dans Coq
In order to develop safer software for critical applications, some static analyzers aim at establishing, with mathematical certitude, the absence of some classes of bug in the input program. A possible limit to this approach is the possibility of a soundness bug in the static analyzer itself, which would nullify the guarantees it is supposed to deliver. In this thesis, we propose to establish formal guarantees on the static analyzer itself: we present the design, implementation and proof of soundness using Coq of Verasco, a formally verified static analyzer based on abstract interpretation handling most of the ISO C99 language, including IEEE754 floating-point arithmetic (except recursion and dynamic memory allocation). Verasco aims at establishing the absence of erroneous behavior of the given programs. It enjoys a modular extendable architecture with several abstract domains and well-specified interfaces. We present the abstract iterator of Verasco, its handling of bounded machine arithmetic, its interval abstract domain, its symbolic abstract domain and its abstract domain of octagons. Verasco led to the development of new techniques for implementing data structure with sharing in Coq

Gli stili APA, Harvard, Vancouver, ISO e altri

18

Gallois-Wong, Diane. "Formalisation en Coq des algorithmes de filtre numérique calculés en précision finie". Electronic Thesis or Diss., université Paris-Saclay, 2021. http://www.theses.fr/2021UPASG016.

Testo completo

Abstract (sommario):

Les filtres numériques sont utilisés dans de nombreux domaines, des télécommunications à l'aérospatiale. En pratique, ces filtres sont calculés sur machine en précision finie (virgule flottante ou virgule fixe). Les erreurs d'arrondi résultantes peuvent être particulièrement problématiques dans les systèmes embarqués. En effet, de fortes contraintes énergétiques et spatiales peuvent amener à privilégier l'efficacité des calculs, souvent au détriment de leur précision. De plus, les algorithmes de filtres enchaînent de nombreux calculs, au cours desquels les erreurs d'arrondi se propagent et risquent de s'accumuler. Comme certains domaines d'application sont critiques, j'analyse les erreurs d'arrondi dans les algorithmes de filtre en utilisant l'assistant de preuve Coq. Il s'agit d'un logiciel qui garantit formellement que cette analyse est correcte. Un premier objectif est d'obtenir des bornes certifiées sur la différence entre les valeurs produites par un filtre implémenté (calculé en précision finie) et par le filtre modèle initial (défini par des calculs théoriques exacts). Un second objectif est de garantir l'absence de comportement catastrophique comme un dépassement de capacité supérieur imprévu. Je définis en Coq les filtres numériques linéaires invariants dans le temps (LTI), considérés dans le domaine temporel. Je formalise une forme universelle appelée la SIF, à laquelle on peut ramener n'importe quel algorithme de filtre LTI sans modifier ses propriétés numériques. Je prouve ensuite le théorème des filtres d'erreurs et le théorème du Worst-Case Peak Gain, qui sont deux théorèmes essentiels à l'analyse numérique d'un filtre sous forme de SIF. Par ailleurs, cette analyse dépend aussi de l'algorithme de somme de produits utilisé dans l'implémentation. Je formalise donc plusieurs algorithmes de somme de produits offrant différents compromis entre précision du résultat et vitesse de calcul, dont un algorithme original correctement arrondi au plus proche. Je définis également en Coq les dépassements de capacité supérieurs modulaires, afin de prouver la correction d'un de ces algorithmes même en présence de tels dépassements de capacité
Digital filters have numerous applications, from telecommunications to aerospace. To be used in practice, a filter needs to be implemented using finite precision (floating- or fixed-point arithmetic). Resulting rounding errors may become especially problematic in embedded systems: tight time, space, and energy constraints mean that we often need to cut into the precision of computations, in order to improve their efficiency. Moreover, digital filter programs are strongly iterative: rounding errors may propagate and accumulate through many successive iterations. As some of the application domains are critical, I study rounding errors in digital filter algorithms using formal methods to provide stronger guaranties. More specifically, I use Coq, a proof assistant that ensures the correctness of this numerical behavior analysis. I aim at providing certified error bounds over the difference between outputs from an implemented filter (computed using finite precision) and from the original model filter (theoretically defined with exact operations). Another goal is to guarantee that no catastrophic behavior (such as unexpected overflows) will occur. Using Coq, I define linear time-invariant (LTI) digital filters in time domain. I formalize a universal form called SIF: any LTI filter algorithm may be expressed as a SIF while retaining its numerical behavior. I then prove the error filters theorem and the Worst-Case Peak Gain theorem. These two theorems allow us to analyze the numerical behavior of the filter described by a given SIF. This analysis also involves the sum-of-products algorithm used during the computation of the filter. Therefore, I formalize several sum-of-products algorithms, that offer various trade-offs between output precision and computation speed. This includes a new algorithm whose output is correctly rounded-to-nearest. I also formalize modular overflows, and prove that one of the previous sum-of-products algorithms remains correct even when such overflows are taken into account

Gli stili APA, Harvard, Vancouver, ISO e altri

19

Garillot, François. "Outils génériques de preuve et théorie des groupes finis". Phd thesis, Ecole Polytechnique X, 2011. http://pastel.archives-ouvertes.fr/pastel-00649586.

Testo completo

Abstract (sommario):

Cette thèse présente des avancées dans l'utilisation des Structures Canoniques, un mécanisme du langage de programmation de l'assistant de preuve Coq, équivalent à la notion de classes de types. Elle fournit un nouveau modèle pour le développement de hiérarchies mathématiques à l'aide d'enregistrements dépendants, et, en guise d'illustration, fournit une reformulation de la preuve formelle de correction du cryptosystème RSA, offrant des méthodes de raisonnement algébrique ainsi que la représentation en théorie des types des notions mathématiques nécessaires (incluant les groupes cycliques, les groupes d'automorphisme, les isomorphismes de groupe). Nous produisons une extension du mécanisme d'inférence de Structures Canoniques à l'aide de types fantômes, et l'appliquons au traitement de fonctions partielles. Ensuite, nous considérons un traitement générique de plusieurs formes de définitions de sous-groupes rencontrées au long de la preuve du théorème de Feit-Thomspon, une large librairie d'algèbre formelle développée au sein de l'équipe Mathematical Components au laboratoire commun MSR-INRIA. Nous montrons qu'un traitement unifié de ces 16 sous-groupes nous permet de raccourcir la preuve de leur propriétés élémentaires, et d'obtenir des définitions offrant une meilleure compositionnalité. Nous formalisons une correspondance entre l'étude de ces fonctorielles, et des propriété de théorie des groupes usuelles, telles que représentées par la classe des groupes qui les vérifie. Nous concluons en explorant les possibilités d'analyse de la fonctorialité de ces définitions par l'inspection de leur type, et suggérons une voie d'approche vers l'obtention d'instances d'un résultat de paramétricité en Coq.

Gli stili APA, Harvard, Vancouver, ISO e altri

20

Anoun, Houda. "Approche logique des grammaires pour les langues naturelles". Phd thesis, Université Sciences et Technologies - Bordeaux I, 2007. http://tel.archives-ouvertes.fr/tel-00414778.

Testo completo

Abstract (sommario):

Les contributions majeures de cette thèse s'articulent autour des trois axes de base de la linguistique computationnelle, à savoir la logique, la linguistique et l'informatique. Nous proposons ainsi un nouveau système non-directionnel GLE permettant de simuler les opérations transformationnelles du Programme Minimaliste dans un cadre logique qui fait appel au raisonnement hypothétique de manière contrôlée. La pertinence de ce formalisme est soulignée en montrant sa capacité à prendre en charge des phénomènes linguistiques complexes, nécessitant un partage contraint de ressources, tels que le liage d'anaphores ou la résolution d'ellipse. En outre, nous présentons un atelier logique, nommé ICHARATE, destiné à la recherche et l'enseignement de la linguistique computationnelle. Cet outil est composé de bibliothèques pour l'assistant à la démonstration Coq, qui comprennent la formalisation de systèmes logiques avancés dédiés au traitement des langues naturelles, dont la logique multimodale.

Gli stili APA, Harvard, Vancouver, ISO e altri

21

Tristan, Jean-Baptiste. "Formal verification of translation validators". Phd thesis, Université Paris-Diderot - Paris VII, 2009. http://tel.archives-ouvertes.fr/tel-00437582.

Testo completo

Abstract (sommario):

Comme tout logiciel, les compilateurs, et tout particulièrement les compilateurs optimisant, peuvent être défectueux. Il est donc possible qu'ils changent la sémantique du programme compilé, et par conséquent ses propriétés. Dans le cadre de développement de logiciels critiques, où des méthodes formelles sont utilisées pour s'assurer qu'un programme satisfait certaines propriétés, et cela avant qu'il soit compilé, cela pose un problème de fond. Une solution à ce problème est de vérifier le compilateur en s'assurant qu'il préserve la sémantique des programmes compilés. Dans cette thèse, nous évaluons une méthode nouvelle pour développer des passes de compilations sûres: la vérification formelle de validateurs de traduction. D'une part, cette méthode utilise la vérification formelle à l'aide d'assistant de preuve afin d'offrir le maximum de garanties de sûreté sur le compilateur. D'autre part, elle repose sur l'utilisation de la validation de traduction, où chaque exécution du compilateur est validée a posteriori, une méthode de vérification plus pragmatique qui a permis de vérifier des optimisations avancées. Nous montrons que cette approche nouvelle du problème de la vérification de compilateur est viable, et même avantageuse dans certains cas, à travers quatre exemples d'optimisations réalistes et agressives: le list scheduling, le trace scheduling, le lazy code motion et enfin le software pipelining.

Gli stili APA, Harvard, Vancouver, ISO e altri

22

Dumbravă, Ştefania-Gabriela. "Formalisation en Coq de Bases de Données Relationnelles et Déductives -et Mécanisation de Datalog". Thesis, Université Paris-Saclay (ComUE), 2016. http://www.theses.fr/2016SACLS525/document.

Testo completo

Abstract (sommario):

Cette thèse présente une formalisation en Coq des langages et des algorithmes fondamentaux portant sur les bases de données. Ainsi, ce fourni des spécifications formelles issues des deux approches différentes pour la définition des modèles de données: une basée sur l’algèbre et l'autre basée sur la logique.A ce titre, une première contribution de cette thèse est le développement d'une bibliothèque Coq pour le modèle relationnel. Cette bibliothèque contient les modélisations de l’algèbre relationnelle et des requêtes conjonctives. Il contient aussi une mécanisation des contraintes d'intégrité et de leurs procédures d'inférence. Nous modélisons deux types de contraintes: les dépendances, qui sont parmi les plus courantes: les dépendances fonctionnelles et les dépendances multivaluées, ainsi que leurs axiomatisations correspondantes. Nous prouvons formellement la correction de leurs algorithmes d'inférence et, pour le cas de dépendances fonctionnelles, aussi la complétude.Ces types de dépendances sont des instances de contraintes plus générales : les dépendances génératrices d'égalité (equality generating dependencies, EGD) et, respectivement, les dépendances génératrices de tuples (tuple generating dependencies, TGD), qui appartiennent a une classe encore plus large des dépendances générales (general dependencies). Nous modélisons ces dernières et leur procédure d'inférence, i.e, "the chase", pour lequel nous établissons la correction. Enfin, on prouve formellement les théorèmes principaux des bases de données, c'est-à-dire, les équivalences algébriques, la théorème de l' homomorphisme et la minimisation des requêtes conjonctives.Une deuxième contribution consiste dans le développement d'une bibliothèque Coq/ssreflect pour la programmation logique, restreinte au cas du Datalog. Dans le cadre de ce travail, nous donnons la première mécanisations d'un moteur Datalog standard et de son extension avec la négation. La bibliothèque comprend une formalisation de leur sémantique en theorie des modelés ainsi que de leur sémantique par point fixe, implémentée par une procédure d'évaluation stratifiée. La bibliothèque est complétée par les preuves de correction, de terminaison et de complétude correspondantes. Cette plateforme ouvre la voie a la certification d' applications centrées données
This thesis presents a formalization of fundamental database theories and algorithms. This furthers the maturing state of the art in formal specification development in the database field, with contributions stemming from two foundational approches to database models: relational and logic based.As such, a first contribution is a Coq library for the relational model. This contains a mechanization of integrity constraints and of their inference procedures. We model two of the most common dependencies, namely functional and multivalued, together with their corresponding axiomatizations. We prove soundness of their inference algorithms and, for the case of functional ones, also completeness. These types of dependencies are instances of equality and, respectively, tuple generating dependencies, which fall under the yet wider class of general dependencies. We model these and their inference procedure,i.e, the chase, for which we establish soundness.A second contribution consists of a Coq/Ssreflect library for logic programming in the Datalog setting. As part of this work, we give (one of the) first mechanizations of the standard Datalog language and of its extension with negation. The library includes a formalization of their model theoretical semantics and of their fixpoint semantics, implemented through bottom-up and, respectively, through stratified evaluation procedures. This is complete with the corresponding soundness, termination and completeness proofs. In this context, we also construct a preliminary framework for dealing with stratified programs. This work paves the way towards the certification of data-centric applications

Gli stili APA, Harvard, Vancouver, ISO e altri

23

Zimmermann, Théo. "Challenges in the collaborative evolution of a proof language and its ecosystem". Thesis, Université de Paris (2019-....), 2019. http://www.theses.fr/2019UNIP7163.

Testo completo

Abstract (sommario):

Dans cette thèse, je présente l'application de méthodes et de connaissances en génie logiciel au développement, à la maintenance et à l'évolution de Coq —un assistant de preuve interactif basé sur la théorie des types— et de son écosystème de paquets. Coq est développé chez Inria depuis 1984, mais sa base d’utilisateurs n’a cessé de s’agrandir, ce qui suscite désormais une attention renforcée quant à sa maintenabilité et à la participation de contributeurs externes à son évolution et à celle de son écosystème de plugins et de bibliothèques.D'importants changements ont eu lieu ces dernières années dans les processus de développement de Coq, dont j'ai été à la fois un témoin et un acteur (adoption de GitHub en tant que plate-forme de développement, tout d'abord pour son mécanisme de pull request, puis pour son système de tickets, adoption de l'intégration continue, passage à des cycles de sortie de nouvelles versions plus courts, implication accrue de contributeurs externes dans les processus de développement et de maintenance open source). Les contributions de cette thèse incluent une description historique de ces changements, le raffinement des processus existants et la conception de nouveaux processus, la conception et la mise en œuvre de nouveaux outils facilitant l’application de ces processus, et la validation de ces changements par le biais d’évaluations empiriques rigoureuses.L'implication de contributeurs externes est également très utile au niveau de l'écosystème de paquets. Cette thèse contient en outre une analyse des méthodes de distribution de paquets et du problème spécifique de la maintenance à long terme des paquets ayant un seul responsable
In this thesis, I present the application of software engineering methods and knowledge to the development, maintenance, and evolution of Coq —an interactive proof assistant based on type theory— and its package ecosystem. Coq has been developed at Inria since 1984, but has only more recently seen a surge in its user base, which leads to much stronger concerns about its maintainability, and the involvement of external contributors in the evolution of both Coq, and its ecosystem of plugins and libraries.Recent years have seen important changes in the development processes of Coq, of which I have been a witness and an actor (adoption of GitHub as a development platform, first for its pull request mechanism, then for its bug tracker, adoption of continuous integration, switch to shorter release cycles, increased involvement of external contributors in the open source development and maintenance process). The contributions of this thesis include a historical description of these changes, the refinement of existing processes, and the design of new ones, the design and implementation of new tools to help the application of these processes, and the validation of these changes through rigorous empirical evaluation.Involving external contributors is also very useful at the level of the package ecosystem. This thesis additionally contains an analysis of package distribution methods, and a focus on the problem of the long-term maintenance of single-maintainer packages

Gli stili APA, Harvard, Vancouver, ISO e altri

24

Jomaa, Narjes. "Le co-design d’un noyau de système d’exploitation et de sa preuve formelle d’isolation". Thesis, Lille 1, 2018. http://www.theses.fr/2018LIL1I075/document.

Testo completo

Abstract (sommario):

Dans cette thèse nous proposons un nouveau concept de noyau adapté à la preuve que nous avons appelé « proto-noyau ». Il s’agit d’un noyau de système d’exploitation minimal où la minimisation de sa taille est principalement motivée par la réduction du coût de la preuve mais aussi de la surface d’attaque. Ceci nous amène à définir une nouvelle stratégie de « co-design » du noyau et de sa preuve. Elle est fondée principalement sur les feedbacks entre les différentes phases de développement du noyau, allant de la définition des besoins jusqu’à la vérification formelle de ses propriétés. Ainsi, dans ce contexte nous avons conçu et implémenté le proto-noyau Pip. L’ensemble de ses appels système a été choisi minutieusement pendant la phase de conception pour assurer à la fois la faisabilité de la preuve et l’utilisabilité du système. Le code de Pip est écrit en Gallina (le langage de spécification de l’assistant de preuve Coq) puis traduit automatiquement vers le langage C. La propriété principale étudiée dans ces travaux est une propriété de sécurité, exprimée en termes d’isolation mémoire. Cette propriété a été largement étudiée dans la littérature de par son importance. Ainsi, nos travaux consistent plus particulièrement à orienter le développement des concepts de base de ce noyau minimaliste par la vérification formelle de cette propriété. La stratégie de vérification a été expérimentée, dans un premier temps, sur un modèle générique de micro-noyau que nous avons également écrit en Gallina. Par ce modèle simplifié de micro-noyau nous avons pu valider notre approche de vérification avant de l’appliquer sur l’implémentation concrète du proto-noyau Pip
In this thesis we propose a new kernel concept adapted to verification that we have called protokernel. It is a minimal operating system kernel where the minimization of its size is motivated by the reduction of the cost of proof and of the attack surface. This leads us to define a new strategy of codesign of the kernel and its proof. It is based mainly on the feedbacks between the various steps of development of the kernel, ranging from the definition of its specification to the formal verification of its properties. Thus, in this context we have designed and implemented the Pip protokernel. All of its system calls were carefully identified during the design step to ensure both the feasibility of proof and the usability of the system. The code of Pip is written in Gallina (the specification language of the Coq proof assistant) and then automatically translated into C code. The main property studied in this work is a security property, expressed in terms of memory isolation. This property has been largely discussed in the literature due to its importance. Thus, our work consists more particularly in guiding the developer to define the fundamental concepts of this minimalistic kernel through the formal verification of its isolation property. The verification strategy was first experimented with a generic microkernel model that we also wrote in Gallina. With this simplified microkernel model we were able to validate our verification approach before applying it to the concrete implementation of the Pip protokernel

Gli stili APA, Harvard, Vancouver, ISO e altri

25

Heraud, Sylvain. "Vérification semi-automatique de primitives cryptographiques". Phd thesis, Université de Nice Sophia-Antipolis, 2012. http://tel.archives-ouvertes.fr/tel-00766757.

Testo completo

Abstract (sommario):

CertiCrypt est une bibliothèque qui permet de vérifier la sécurité exacte de primitives cryptographiques dans l'assistant à la preuve Coq. CertiCrypt instrumente l'approche des preuves par jeux, et repose sur de nombreux domaines comme les probabilités, la complexité, l'algèbre, la sémantique des langages de programmation, et les optimisations de programmes. Dans cette thèse, nous présentons deux exemples d'utilisation d'EasyCrypt: le schéma d'encryption Hashed ElGamal, et les protocoles à connaissance nulle. Ces exemples, ainsi que les travaux antérieurs sur CertiCrypt, démontrent qu'il est possible de formaliser des preuves complexes; toutefois, l'utilisation de CertiCrypt demande une bonne expertise en Coq, et demeure laborieuse. Afin de faciliter l'adoption des preuves formelles par la communauté cryptographique, nous avons développé EasyCrypt, un outil semi-automatique capable de reconstruire des preuves formelles de sécurité à partir d'une ébauche formelle de preuve. EasyCrypt utilise des outils de preuves automatiques pour vérifier les ébauches de preuves, puis les compiles vers des preuves vérifiables avec CertiCrypt. Nous validons EasyCrypt en prouvant à nouveau Hashed ElGamal, et comparons cette nouvelle preuve avec celle en CertiCrypt. Nous prouvons également le schéma d'encryption Cramer-Shoup. Enfin, nous expliquerons comment étendre le langage de CertiCrypt à des classes de complexité implicite, permettant de modéliser la notion de fonctions en temps polynomial.

Gli stili APA, Harvard, Vancouver, ISO e altri

26

Rouhling, Damien. "Outils pour la formalisation en analyse classique : une étude de cas en théorie du contrôle". Thesis, Université Côte d'Azur (ComUE), 2019. http://www.theses.fr/2019AZUR4058.

Testo completo

Abstract (sommario):

Il s'agit de mettre à l'épreuve une bibliothèque d'analyse dans l'assistant de preuve Coq au travers d'une étude de cas en théorie du contrôle. Nous formalisons une preuve de stabilité pour le pendule inversé, un exemple classique en théorie du contrôle. Le contrôle du pendule inversé est un défi en raison de sa non-linéarité, à tel point que ce système est souvent utilisé comme référence pour l'essai de nouvelles techniques de contrôle. Durant cette étude de cas, nous identifions des défauts des outils aujourd'hui accessibles pour la formalisation en analyse classique et nous en développons d'autres afin d'atteindre le but de cette étude de cas. En particulier, nous essayons d'imiter le style de preuve sur papier grâce à de nouvelles notations et de nouveaux mécanismes d'inférence. C'est une étape essentielle pour rendre la preuve formelle plus accessible aux mathématiciens. Ensuite, nous développons une nouvelle bibliothèque d'analyse classique en Coq, qui intègre ces nouveaux outils et qui essaie de pallier les limitations de la bibliothèque que nous avons testée, en particulier dans le domaine du raisonnement asymptotique. Nous testons aussi cette nouvelle bibliothèque sur la même preuve formelle et tirons des conclusions sur ses forces et faiblesses. Enfin, nous esquissons une nouvelle méthodologie pour répondre aux limitations de notre bibliothèque dans le domaine du calcul. Nous exploitons une technique appelée raffinement afin de refactoriser la méthode de preuve par réflexion, une technique qui automatise les preuves grâce au calcul et qui de plus réduit la taille des termes de preuves. Nous mettons en œuvre cette méthodologie sur l'exemple du raisonnement arithmétique dans les anneaux et expliquons comment ce travail pourrait servir à généraliser des outils déjà existants
In this thesis, we put a library for analysis in the Coq proof assistant to the test through a case study in control theory. We formalise a proof of stability for the inverted pendulum, a standard example in control theory. Controlling the inverted pendulum is challenging because of its non-linearity, so that this system is often used as a benchmark for new control techniques. Through this case study, we identify issues in the tools that are currently available for the formalisation of classical analysis and we develop new ones in order to achieve our formalisation goal. In particular, we try to imitate the pen-and-paper proof style thanks to new notations and inference mechanisms. This is an essential step to make formal proofs more accessible to mathematicians. We then develop a new library for classical analysis in Coq that integrates these new tools and tries to palliate the limitations of the library we tested, especially in the domain of asymptotic reasoning. We also experiment with this new library on the same formal proof and draw lessons on its strengths and weaknesses. Finally, we sketch a new methodology in order to address the limitations of our library in the particular domain of computation. We exploit a technique called refinement to refactor the methodology of proof by reflection, a technique that automates proofs through computation and also reduces the size of proof terms. We implement this methodology on the example of arithmetic reasoning in rings and discuss how this work could be used to generalise existing tools

Gli stili APA, Harvard, Vancouver, ISO e altri

27

Benayoun, Vincent. "Analyse de dépendances ML pour les évaluateurs de logiciels critiques". Phd thesis, Conservatoire national des arts et metiers - CNAM, 2014. http://tel.archives-ouvertes.fr/tel-01062785.

Testo completo

Abstract (sommario):

Les logiciels critiques nécessitent l'obtention d'une évaluation de conformité aux normesen vigueur avant leur mise en service. Cette évaluation est obtenue après un long travaild'analyse effectué par les évaluateurs de logiciels critiques. Ces derniers peuvent être aidéspar des outils utilisés de manière interactive pour construire des modèles, en faisant appel àdes analyses de flots d'information. Des outils comme SPARK-Ada existent pour des sous-ensembles du langage Ada utilisés pour le développement de logiciels critiques. Cependant,des langages émergents comme ceux de la famille ML ne disposent pas de tels outils adaptés.La construction d'outils similaires pour les langages ML demande une attention particulièresur certaines spécificités comme les fonctions d'ordre supérieur ou le filtrage par motifs. Cetravail présente une analyse de flot d'information pour de tels langages, spécialement conçuepour répondre aux besoins des évaluateurs. Cette analyse statique prend la forme d'uneinterprétation abstraite de la sémantique opérationnelle préalablement enrichie par desinformations de dépendances. Elle est prouvée correcte vis-à-vis d'une définition formellede la notion de dépendance, à l'aide de l'assistant à la preuve Coq. Ce travail constitue unebase théorique solide utilisable pour construire un outil efficace pour l'analyse de toléranceaux pannes.

Gli stili APA, Harvard, Vancouver, ISO e altri

28

Tollitte, Pierre-Nicolas. "Extraction de code fonctionnel certifié à partir de spécifications inductives". Phd thesis, Conservatoire national des arts et metiers - CNAM, 2013. http://tel.archives-ouvertes.fr/tel-00968607.

Testo completo

Abstract (sommario):

Les outils d'aide à la preuve basés sur la théorie des types permettent à l'utilisateur d'adopter soit un style fonctionnel, soit un style relationnel (c'est-à-dire en utilisant des types inductifs). Chacun des deux styles a des avantages et des inconvénients. Le style relationnel peut être préféré parce qu'il permet à l'utilisateur de décrire seulement ce qui est vrai, de s'abstraire temporairement de la question de la terminaison, et de s'en tenir à une description utilisant des règles. Cependant, une spécification relationnelle n'est pas exécutable.Nous proposons un cadre général pour transformer une spécification inductive en une spécification fonctionnelle, en extrayant à partir de la première une fonction et en produisant éventuellement la preuve de correction de la fonction extraite par rapport à sa spécification inductive. De plus, à partir de modes définis par l'utilisateur, qui permettent de considérer les arguments de la relation comme des entrées ou des sorties (de fonction), nous pouvons extraire plusieurs comportements calculatoires à partir d'un seul type inductif.Nous fournissons également deux implantations de notre approche, l'une dans l'outil d'aide à la preuve Coq et l'autre dans l'environnement Focalize. Les deux sont actuellement distribuées avec leurs outils respectifs.

Gli stili APA, Harvard, Vancouver, ISO e altri

29

Tollitte, Pierre-Nicolas. "Extraction de code fonctionnel certifié à partir de spécifications inductives". Electronic Thesis or Diss., Paris, CNAM, 2013. http://www.theses.fr/2013CNAM0895.

Testo completo

Abstract (sommario):

Les outils d’aide à la preuve basés sur la théorie des types permettent à l’utilisateur d’adopter soit un style fonctionnel, soit un style relationnel (c’est-à-dire en utilisant des types inductifs). Chacun des deux styles a des avantages et des inconvénients. Le style relationnel peut être préféré parce qu’il permet à l’utilisateur de décrire seulement ce qui est vrai, de s’abstraire temporairement de la question de la terminaison, et de s’en tenir à une description utilisant des règles. Cependant, une spécification relationnelle n’est pas exécutable.Nous proposons un cadre général pour transformer une spécification inductive en une spécification fonctionnelle, en extrayant à partir de la première une fonction et en produisant éventuellement la preuve de correction de la fonction extraite par rapport à sa spécification inductive. De plus, à partir de modes définis par l’utilisateur, qui permettent de considérer les arguments de la relation comme des entrées ou des sorties (de fonction), nous pouvons extraire plusieurs comportements calculatoires à partir d’un seul type inductif.Nous fournissons également deux implantations de notre approche, l’une dans l’outil d’aide à la preuve Coq et l’autre dans l’environnement Focalize. Les deux sont actuellement distribuées avec leurs outils respectifs
Proof assistants based on type theory allow the user to adopt either a functional style, or a relational style (e.g., by using inductive types). Both styles have advantages and drawbacks. Relational style may be preferred because it allows the user to describe only what is true, discard momentarily the termination question, and stick to a rule-based description. However, a relational specification is usually not executable.We propose a general framework to turn an inductive specification into a functional one, by extracting a function from the former and eventually produce the proof of soundness of the extracted function w.r.t. its inductive specification. In addition, using user-defined modes which label inputs and outputs, we are able to extract several computational contents from a single inductive type.We also provide two implementations of our approach, one in the Coq proof assistant and the other in the Focalize environnement. Both are currently distributed with the respective tools

Gli stili APA, Harvard, Vancouver, ISO e altri

30

Duclos, Mathilde. "Méthodes pour la vérification des protocoles cryptographiques dans le modèle calculatoire". Thesis, Université Grenoble Alpes (ComUE), 2016. http://www.theses.fr/2016GREAM002/document.

Testo completo

Abstract (sommario):

Les échanges des informations confidentielles ou critiques dans un environnement public, et donc potentiellement hostile, nécessitent l'emploi de techniques cryptographiques (protocoles et primitives). Malheureusement, l'expérience montre qu'une mauvaise conception, ou une expression peu claire des propriétés et hypothèses de sécurité attendues conduisent à des attaques, et qu'il faut parfois des années avant que celles-ci soient découvertes et corrigées. D'où l'adoption croissante de la sécurité prouvable, où on donne une définition rigoureuse des objectifs de sécurité et des démonstrations mathématiques que ceux-ci sont remplis. Par ailleurs, la complexité et la diversité des systèmes cryptographiques croît également. Il est donc largement admis qu'il n'est plus viable d'écrire ou vérifier manuellement des démonstrations cryptographiques (Bellare& Rogaway 2004, Shoup 2004, Halevi 2005) et qu'il faut développer des méthodes de vérification des systèmes cryptographiques assistées par ordinateur. L'objectif de cette thèse est d'effectuer des progrès significatifs dans cette direction. Plus précisement on s'interesse à la preuve formelle de protocoles cryptographiques. Vérifier des protocoles cryptographiques requiert le développement d'un cadre théorique qui doit permettre: - une modélisation précise des protocoles cryptographiques et des propriétés de sécurité qu'on veut prouver dans le modèle calculatoire. - mise en place de stratégies d'automatisation de preuves. - prise en compte des modèles plus réalistes pour l'adversaire (canaux cachés, ressources de calcul). A la fin de la thèse on a obtenu un cadre formel et un ensemble de méthodes logicielles capable d'aider à la vérification des protocoles cryptographiques
Critical and private information are exchanged on public environment. To protect it from dishonest users, we use cryptographic tools. Unfortunately, bad conception, poorly written security properties and required security hypothesis lead to attacks, and it may take years before one discover the attack and fix the security schemes involved. In this context, provable security provides formal definitions for security objectives and implied mathematical proofs that these objectives are fullfilled. On another hand, complexity and variety of cryptographic systems are increasing, and proofs by hand are too complicated to write and to verify (Bellare& Rogaway 2004, Shoup 2004, Halevi 2005). Thus, we need computer-assisted verification methods for cryptographic systems. The aim of this thesis is to progress in this direction. More precisely we want significant progress over formal proofs on cryptographic protocols. To verify cryptographic protocols we need to develop a theoritical framework providing: - a precise modelisation for cryptographic protocols and security properties we want to prove in the computationnal model, - designing tactics to automate proofs, - taking into account realistic models for adversary (side-channels...). By the end of the thesis we have enhanced a theoretical framework and computing tools helping verifying cryptographic protocols

Gli stili APA, Harvard, Vancouver, ISO e altri

31

Siles, Vincent. "Etude sur le typage de l'égalité dans les systèmes de types". Phd thesis, Ecole Polytechnique X, 2010. http://pastel.archives-ouvertes.fr/pastel-00556578.

Testo completo

Abstract (sommario):

Le travail présenté dans cette thèse concerne l'étude de la notion de conversion inhérente à tous système de types dépendants. Plusieurs présentations de ces systèmes ont été étudiées pour des usages variés: typage, recherche de preuve, cohérence de logique... Chacune de ces représentation est accompagnée d'une notion d'égalité différente, suivant les besoins du moment. Mais il n'est pas certains que toutes ces représentations parlent en fin de compte d'une seule et même logique. Nous nous intéressons ici à une famille assez conséquente de systèmes de types, appelés Systèmes de Types Purs, et nous allons prouver que pour ces systèmes, toutes les représentations habituellement utilisées sont en fait équivalentes, c'est à dire qu'il existe des traductions constructives entre chacune de ces présentations. Ces traductions reposent toutes sur la manière de porter une égalité d'un système à l'autre. Ce travail se concentre donc sur les mécanismes de ces égalités, et prouve qu'il est possible de typer n'importe quelle égalité syntaxique en égalité sémantique, et ainsi qu'il est donc possible de passer d'un système à l'autre. L'intégralité de cette thèse a en outre été vérifiée et certifiée correcte à l'aide de l'assistant à la preuve Coq, qui a activement été utilisé tout au long de l'élaboration des preuves. ~

Gli stili APA, Harvard, Vancouver, ISO e altri

32

Lu, Weiyun. "Formally Verified Code Obfuscation in the Coq Proof Assistant". Thesis, Université d'Ottawa / University of Ottawa, 2019. http://hdl.handle.net/10393/39994.

Testo completo

Abstract (sommario):

Code obfuscation is a software security technique where transformations are applied to source and/or machine code to make them more difficult to analyze and understand to deter reverse-engineering and tampering. However, in many commercial tools, such as Irdeto's Cloakware product, it is not clear why the end user should believe that the programs that come out the other end are still the same program"! In this thesis, we apply techniques of formal specification and verification, by using the Coq Proof Assistant and IMP (a simple imperative language within it), to formulate what it means for a program's semantics to be preserved by an obfuscating transformation, and give formal machine-checked proofs that these properties hold. We describe our work on opaque predicate and control flow flattening transformations. Along the way, we also employ Hoare logic as an alternative to state equivalence, as well as augment the IMP program with Switch statements. We also define a lower-level flowchart language to wrap around IMP for modelling certain flattening transformations, treating blocks of codes as objects in their own right. We then discuss related work in the literature on formal verification of data obfuscation and layout obfuscation transformations in IMP, and conclude by discussing CompCert, a formally verified C compiler in Coq, along with work that has been done on obfuscation there, and muse on the possibility of implementing formal methods in the next generation of real-world obfuscation tools.

Gli stili APA, Harvard, Vancouver, ISO e altri

33

Brun, Lélio. "Sémantique mécanisée et compilation vérifiée pour un langage synchrone à flots de données avec réinitialisation". Thesis, Université Paris sciences et lettres, 2020. http://www.theses.fr/2020UPSLE003.

Testo completo

Abstract (sommario):

Les spécifications basées sur les schémas-blocs et machines à états sont utilisées pour la conception de systèmes de contrôle-commande, particulièrement dans le développement d'applications critiques. Des outils tels que Scade et Simulink/Stateflow sont équipés de compilateurs qui traduisent de telles spécifications en code exécutable. ls proposent des langages de programmation permettant de composer des fonctions sur des flots, tel que l'illustre le langage synchrone à flots de données Lustre. Cette thèse présente Vélus, un compilateur Lustre vérifié dans l'assistant de preuves interactif Coq. Nous développons des modèles sémantiques pour les langages de la chaîne de compilation, et utilisons le compilateur C vérifié CompCert pour générer du code exécutable et donner une preuve de correction de bout en bout. Le défi principal est de montrer la préservation de la sémantique entre le paradigme flots de données et le paradigme impératif, et de raisonner sur la représentation bas niveau de l'état d'un programme. En particulier, nous traitons le reset modulaire, une primitive pour réinitialiser des sous-systèmes. Ceci implique la mise en place de modèles sémantiques adéquats, d'algorithmes de compilation et des preuves de correction correspondantes. Nous présentons un nouveau langage intermédiaire dans le schéma habituel de compilation modulaire dirigé par les horloges de Lustre. Ceci débouche sur l'implémentation de passes de compilation permettant de générer un meilleur code séquentiel, et facilite le raisonnement sur la correction des transformations successives du reset modulaire
Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like Scade and Simulink/Stateflow are equipped with compilers that translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by dataflow synchronous languages like Lustre. In this thesis we present Vélus, a Lustre compiler verified in the interactive theorem prover Coq. We develop semantic models for the various languages in the compilation chain, and build on the verified CompCert C compiler to generate executable code and give an end-to-end correctness proof. The main challenge is to show semantic preservation between the dataflow paradigm and the imperative paradigm, and to reason about byte-level representations of program states. We treat, in particular, the modular reset construct, a primitive for resetting subsystems. This necessitates the design of suitable semantic models, compilation algorithms and corresponding correctness proofs. We introduce a novel intermediate language into the usual clock-directed modular compilation scheme of Lustre. This permits the implementation of compilation passes that generate better sequential code, and facilitates reasoning about the correctness of the successive transformations of the modular reset construct

Gli stili APA, Harvard, Vancouver, ISO e altri

34

Benayoun, Vincent. "Analyse de dépendances ML pour les évaluateurs de logiciels critiques". Electronic Thesis or Diss., Paris, CNAM, 2014. http://www.theses.fr/2014CNAM0915.

Testo completo

Abstract (sommario):

Les logiciels critiques nécessitent l’obtention d’une évaluation de conformité aux normesen vigueur avant leur mise en service. Cette évaluation est obtenue après un long travaild’analyse effectué par les évaluateurs de logiciels critiques. Ces derniers peuvent être aidéspar des outils utilisés de manière interactive pour construire des modèles, en faisant appel àdes analyses de flots d’information. Des outils comme SPARK-Ada existent pour des sous-ensembles du langage Ada utilisés pour le développement de logiciels critiques. Cependant,des langages émergents comme ceux de la famille ML ne disposent pas de tels outils adaptés.La construction d’outils similaires pour les langages ML demande une attention particulièresur certaines spécificités comme les fonctions d’ordre supérieur ou le filtrage par motifs. Cetravail présente une analyse de flot d’information pour de tels langages, spécialement conçuepour répondre aux besoins des évaluateurs. Cette analyse statique prend la forme d’uneinterprétation abstraite de la sémantique opérationnelle préalablement enrichie par desinformations de dépendances. Elle est prouvée correcte vis-à-vis d’une définition formellede la notion de dépendance, à l’aide de l’assistant à la preuve Coq. Ce travail constitue unebase théorique solide utilisable pour construire un outil efficace pour l’analyse de toléranceaux pannes
Critical software needs to obtain an assessment before commissioning in order to ensure compliance tostandards. This assessment is given after a long task of software analysis performed by assessors. Theymay be helped by tools, used interactively, to build models using information-flow analysis. Tools likeSPARK-Ada exist for Ada subsets used for critical software. But some emergent languages such as thoseof the ML family lack such adapted tools. Providing similar tools for ML languages requires specialattention on specific features such as higher-order functions and pattern-matching. This work presentsan information-flow analysis for such a language specifically designed according to the needs of assessors.This analysis is built as an abstract interpretation of the operational semantics enriched with dependencyinformation. It is proved correct according to a formal definition of the notion of dependency using theCoq proof assistant. This work gives a strong theoretical basis for building an efficient tool for faulttolerance analysis

Gli stili APA, Harvard, Vancouver, ISO e altri

35

Pasca, Ioana. "Vérification formelle pour les méthodes numériques". Phd thesis, Université de Nice Sophia-Antipolis, 2010. http://tel.archives-ouvertes.fr/tel-00555158.

Testo completo

Abstract (sommario):

Cette thèse s'articule autour de la formalisation de mathématiques dans l'assistant à la preuve Coq dans le but de vérifier des méthodes numériques. Plus précisément, elle se concentre sur la formalisation de concepts qui apparaissent dans la résolution des systèmes d'équations linéaires et non-linéaires.

Dans ce cadre, on a analysé la méthode de Newton, couramment utilisée pour approcher les solutions d'une équation ou d'un système d'équations. Le but a été de formaliser le théorème de Kantorovitch qui montre la convergence de la méthode de Newton vers une solution, l'unicité de la solution dans un voisinage, la vitesse de convergence et la stabilité locale de la méthode. L'étude de ce théorème a nécessité la formalisation de concepts d'analyse multivariée. En se basant sur ces résultats classiques sur la méthode de Newton, on a montré qu'arrondir à chaque étape préserve la convergence de la méthode, avec une corrélation bien déterminée entre la précision des données d'entrée et celle du résultat. Dans un travail commun avec Nicolas Julien nous avons aussi formellement étudié les calculs avec la méthode de Newton effectués dans le cadre d'une bibliothèque d'arithmétique réelle exacte.

Pour les systèmes linéaires d'équations, on s'est intéressé aux systèmes qui ont une matrice associée à coefficients intervalles. Pour résoudre de tels systèmes, un problème important qui se pose est de savoir si la matrice associée est régulière. On a fourni la vérification formelle d'une collection de critères de régularité pour les matrices d'intervalles.

Gli stili APA, Harvard, Vancouver, ISO e altri

36

Mahboubi, Assia. "Contributions à la certification des calculs dans R : théorie, preuves, programmation". Phd thesis, Université de Nice Sophia-Antipolis, 2006. http://tel.archives-ouvertes.fr/tel-00117409.

Testo completo

Abstract (sommario):

Le logiciel Coq est un assistant à la preuve basé sur le Calcul des
Constructions Inductives.
Dans cette thèse nous proposons d'améliorer l'automatisation de ce
système en le dotant d'une procédure de décision réflexive et complète
pour la théorie du premier ordre de l'arithmétique réelle.
La théorie des types implémentée par le système Coq comprend un
langage fonctionnel typé dans lequel nous avons programmé un
algorithme de Décomposition Algébrique Cylindrique (CAD). Cet
algorithme calcule une partition de l'espace en cellules
semi-algébriques sur lesquelles tous les polynômes d'une famille donnée
ont un signe constant et permet ainsi de décider les formules de cette théorie.
Il s'agit ensuite de prouver la correction de l'algorithme et de la
procédure de décision associée avec l'assistant à la preuve Coq.
Ce travail comprend en particulier une librairie d'arithmétique polynomiale
certifiée et une partie significative de la preuve formelle de correction de
l'algorithme des sous-résultants. Ce dernier algorithme permet de calculer
efficacement le plus grand commun diviseur de polynômes à coefficients dans un
anneau, en particulier à plusieurs variables.
Nous proposons également une tactique réflexive de décision des égalités dans les
structures d'anneau et de semi-anneaux qui améliore les performances de l'outil
déjà disponible et augmente son spectre d'action en exploitant les possibilités de
calcul du système.
Dans une dernière partie, nous étudions le contenu calculatoire d'une preuve
constructive d'un lemme élémentaire d'analyse réelle, le principe d'induction
ouverte.

Gli stili APA, Harvard, Vancouver, ISO e altri

37

Athalye, Anish (Anish R. ). "CoqIOA : a formalization of IO automata in the Coq proof assistant". Thesis, Massachusetts Institute of Technology, 2017. http://hdl.handle.net/1721.1/112831.

Testo completo

Abstract (sommario):

Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2017.
This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.
Cataloged from student-submitted PDF version of thesis.
Includes bibliographical references (pages 51-53).
Implementing distributed systems correctly is difficult. Designing correct distributed systems protocols is challenging because designs must account for concurrent operation and handle network and machine failures. Implementing these protocols is challenging as well: it is difficult to avoid subtle bugs in implementations of complex protocols. Formal verification is a promising approach to ensuring distributed systems are free of bugs, but verification is challenging and time-consuming. Unfortunately, current approaches to mechanically verifying distributed systems in proof assistants using deductive verification do not allow for modular reasoning, which could greatly reduce the effort required to implement verified distributed systems by enabling reuse of code and proofs. This thesis presents CoqIOA, a framework for reasoning about distributed systems in a compositional way. CoqIOA builds on the theory of input/output automata to support specification, proof, and composition of systems within the proof assistant. The framework's implementation of the theory of IO automata, including refinement, simulation relations, and composition, are all machine-checked in the Coq proof assistant. An evaluation of CoqIOA demonstrates that the framework enables compositional reasoning about distributed systems within the proof assistant.
by Anish Athalye.
M. Eng.

Gli stili APA, Harvard, Vancouver, ISO e altri

38

Thévenon, Patrick. "Vers un assistant à la preuve en langue naturelle". Chambéry, 2006. http://www.theses.fr/2006CHAMS036.

Testo completo

Abstract (sommario):

Cette Thèse est la conclusion de trois ans de travail sur un projet nommé DemoNat. Le but de ce projet est la conception d'un système d'analyse et de vérification de démonstrations mathématiques écrites en langue naturelle. L'architecture générale du système se décrit en 4 phases : 1. Analyse de la démonstration par des outils linguistiques ; 2. Traduction de la démonstration dans un langage restreint ; 3. Interprétation du texte traduit en un arbre de règles de déduction ; 4. Validation des règles de déduction à l'aide d'un démonstrateur automatique. Ce projet a mobilisé des équipes de linguistes et de logiciens, les deux premières phases étant la tâche des linguistes, et les deux dernières étant la tâche des logiciens. Cette thèse présente plus en détail ce projet et développe principalement les points suivants : - définition du langage restreint et de son interprétation ; - propriétés du type principal de termes d'un λ -calcul typé avec deux flèches entrant dans le cadre d'un outil linguistique, les ACGs ; - description du démonstrateur automatique
This Thesis is the conclusion of three years of work in a project named DemoNat. The aim of this project is to design a system able to analyse and validate mathematical proofs written in a natural language. The general scheme of the system is the following : 1. Analysis of the proof by means of linguistics tools ; 2. Translation of the proof in a restricted language ; 3. Interpretation of the translated text in a deduction rules tree ; 4. Validation of the deduction rules with an automatic prover. This project envolved teams of linguists and logicians, the first two phases being the task of the linguists, and the lasts ones being the task of the logicians. This thesis presents in more details the project and develops mainly the following points: - Definition of the restricted language and its interpretation ; - proprerties of the principal type of terms of a typed λ-calculus with two arrows, part of a linguistic tool, the ACGs ; - Description of the automatic prover

Gli stili APA, Harvard, Vancouver, ISO e altri

39

Lasson, Marc. "Réalisabilité et paramétricité dans les systèmes de types purs". Phd thesis, Ecole normale supérieure de lyon - ENS LYON, 2012. http://tel.archives-ouvertes.fr/tel-00770669.

Testo completo

Abstract (sommario):

Cette thèse porte sur l'adaptation de la réalisabilité et la paramétricité au cas des types dépendants dans le cadre des Systèmes de Types Purs. Nous décrivons une méthode systématique pour construire une logique à partir d'un langage de programmation, tous deux décrits comme des systèmes de types purs. Cette logique fournit des formules pour exprimer des propriétés des programmes et elle offre un cadre formel adéquat pour développer une théorie de la réalisabilité au sein de laquelle les réalisateurs des formules sont exactement les programmes du langage de départ. Notre cadre permet alors de considérer les théorèmes de représentation pour le système T de Gödel et le système F de Girard comme deux instances d'un théorème plus général.Puis, nous expliquons comment les relations logiques de la théorie de la paramétricité peuvent s'exprimer en terme de réalisabilité, ce qui montre que la logique engendrée fournit un cadre adéquat pour développer une théorie de la paramétricité du langage de départ. Pour finir, nous montrons comment cette théorie de la paramétricité peut-être adaptée au système sous-jacent à l'assistant de preuve Coq et nous donnons un exemple d'application original de la paramétricité à la formalisation des mathématiques.

Gli stili APA, Harvard, Vancouver, ISO e altri

40

Soubiran, Elie. "Modular development of theories and name-space management for the Coq proof assistant". Palaiseau, Ecole polytechnique, 2010. http://tel.archives-ouvertes.fr/docs/00/67/92/01/PDF/these.pdf.

Testo completo

Abstract (sommario):

Proof assistants offer a formal framework for formalizing and mechanically checking mathematical knowledge. Moreover, due to the numerous applications that follow from formal methods, the scientifc production being formalized and verified by such tools is constantly growing. In that context, the organization and the classification of this knowledge does not have to be neglected. Coq is a proof assistant well-suited for program certification and mathematical formalization, and for seven years now it has featured a module system that helps users in their development processes. Modules provide a way to represent theories and offer a namespace management that is crucial for large developments. In this dissertation, we advance the module system of Coq by putting the emphasis on the two latter aspects. We propose to unify both module implementation and module type into a single notion of structure, and to split our module system in two parts. We have, on one hand, a namespace system that is able to define extensible naming scopes and to deal with renaming, and on the other hand a structure system that describes how to combine and to form structures. We define a new merge operator that, given two structures, builds the resulting structure by unifying components of the former two. In that dual system, a module is the association of a sub-namespace and a pair of structures, it acts as concrete declared theory. Furthermore, we adopt an applicative semantic for higher-order functors that allows a precise propagation of information. We show that this module system is a conservative extension of the underlying base language of Coq and we present the on-going implementation.

Gli stili APA, Harvard, Vancouver, ISO e altri

41

Vinogradova, Polina. "Formalizing Abstract Computability: Turing Categories in Coq". Thesis, Université d'Ottawa / University of Ottawa, 2017. http://hdl.handle.net/10393/36354.

Testo completo

Abstract (sommario):

The concept of a recursive function has been extensively studied using traditional tools of computability theory. However, with the development of category-theoretic methods it has become possible to study recursion in a more general (abstract) sense. The particular model this thesis is structured around is known as a Turing category. The structure within a Turing category models the notion of partiality as well as recursive computation, and equips us with the tools of category theory to study these concepts. The goal of this work is to build a formal language description of this computation model. Specifically, to use the Coq proof assistant to formulate informal definitions, propositions and proofs pertaining to Turing categories in the underlying formal language of Coq, the Calculus of Co-inductive Constructions (CIC). Furthermore, we have instantiated the more general Turing category formalism with a CIC description of the category which models the language of partial recursive functions exactly.

Gli stili APA, Harvard, Vancouver, ISO e altri

42

Fouilhé, Alexis. "Le domaine abstrait des polyèdres revisité : représentation par contraintes et preuve formelle". Thesis, Université Grenoble Alpes (ComUE), 2015. http://www.theses.fr/2015GREAM045/document.

Testo completo

Abstract (sommario):

Cette thèse revisite de deux manières le domaine abstrait des polyèdres utilisé pour l'analyse statique de programmes.D'abord, elle montre comment utiliser l'assistant à la preuve Coq pour apporter des garanties sur la correction des opérations sur les polyèdres sans compromettre l'efficacité de l'outil VP Lissu de ces travaux.L'outil est fondé sur le principe de la vérification de résultats :un oracle, auquel on ne fait pas confiance, fait les calculs,puis les résultats sont vérifiés par un validateur dont la correction est prouvée avec Coq. De plus, l'oracle fournit des témoins de la correction des résultats afin d'accélérer la vérification.L'autre caractéristique de VPL est l' utilsation de la seule représentation par contraintes des polyèdres,par opposition à l'approche habituelle qui consiste à utiliser à la fois des contraintes et des générateurs.Malgré ce choix inhabituel,les performances de VPL s'avèrent compétitives.Comme on pouvait le prévoir,l'opérateur "join",qui calcule l'enveloppe convexe de deux polyèdres,est le plus coûteux.Puisqu'il nécessite un grand nombre de projections,cette thèse explore plusieurs nouvelles approches de l'opérateur de projection,basées sur la programmation linéaire paramétrique.Elle propose une synthèse des variantes et des combinaisons possibles.La thèse se termine sur les éléments clés d'un nouvel algorithme de résolution tirant parti des spécificités de l'encodage afin d'obtenir de bonnes performances
The work reported in this thesis revisits in two waysthe abstract domain of polyhedraused for static analysis of programs.First, strong guarantees are provided on the soundness of the operationson polyhedra,by using of the Coq proof assistant to check the soundness proofs.The means used to ensure correctnessdon't hinder the performance of the resultingVerimag Polyhedra Library (VPL).It is built on the principle of result verification:computations are performed by an untrusted oracleand their results are verified by a checkerwhose correctness is proved in Coq.In order to make verification cheap,the oracle computes soundness witnesses along with the results.The other distinguishing feature of VPL is thatit relies only on the constraint representation of polyhedra,as opposed to the common practice of using both constraints and generators.Despite this unusual choice,VPL turns out to be a competitive abstract domain of polyhedra,performance-wise.As expected, the join operator of VPL,which performs the convex hull of two polyhedra,is the costliest operator.Since it builds on the projection operator,this thesis also investigates a new approach toperforming projections,based on parametric linear programming.A new understanding of projection encoded asa parametric linear problem is presented.The thesis closes on a progress report in the design of a new solvingalgorithm,tailored to the specifics of the encodingso as to achieve good performance

Gli stili APA, Harvard, Vancouver, ISO e altri

43

Braibant, Thomas. "Algèbres de Kleene, réécriture modulo AC et circuits en coq". Phd thesis, Université de Grenoble, 2012. http://tel.archives-ouvertes.fr/tel-00683661.

Testo completo

Abstract (sommario):

Cette thèse décrit trois travaux de formalisation en Coq. Le premier chapitre s'intéresse à l'implémentation d'une procédure de décision efficace pour les algèbres de Kleene, pour lesquelles le modèle des langages réguliers est initial : il est possible de décider la théorie équationelle des algèbres de Kleene via la construction et la comparaison d'automates finis. Le second chapitre est consacré à la définition de tactiques pour la réécriture modulo associativité et commutativité en utilisant deux composants : une procédure de décision réflexive pour l'égalité modulo AC, ainsi qu'un greffon OCaml implémentant le filtrage modulo AC. Le dernier chapitre esquisse une formalisation des circuits digitaux via un plongement profond utilisant les types dépendants de Coq ; on s'intéresse ensuite à prouver la correction totale de circuits paramétriques.

Gli stili APA, Harvard, Vancouver, ISO e altri

44

Glondu, Stéphane. "Vers une certification de l'extraction de coq". Paris 7, 2012. http://www.theses.fr/2012PA077089.

Testo completo

Abstract (sommario):

L'assistant de preuve Coq permet de s'assurer mécaniquement de la correction de chaque étape de raisonnement dans une preuve. Ce système peut également servir au développement de programmes certifiés. En effet, Coq utilise en interne un langage typé dérivé du lambda-calcul, le calcul des constructions inductives (CIC). Ce langage est directement utilisable pour programmer, et un mécanisme, l'extraction, permet de traduire les programmes CIC vers des langages à plus large audience tels qu'OCaml, Haskell ou Scheme. L'extraction n'est pas un simple changement de syntaxe: CIC dispose d'un système de types très riche, mais en contrepartie, des entités purement logiques peuvent apparaître dans les programmes et impacter leurs performances. L'extraction se charge également d'effacer ces parties logiques. Dans cette thèse, nous nous attaquons à la certification de l'extraction elle-même. Nous avons prouvé sa correction dans le cadre d'une formalisation entière de Coq en Coq. Cette formalisation ne correspond pas exactement au CIC implanté dans Coq, mais nous avons tout de même réalisé notre étude avec l'implantation concrète de Coq en tête. Nous proposons également une nouvelle méthode de certification des programmes extraits, dans le cadre concret du système Coq existant
The Coq proof assistant mechanically checks the consistency of the logical reasoning in a proof. It can also be used to develop certified programs. Indeed, Coq uses intemally a typed language derived from lambda-calculus, the calculus of inductive constructions (CIC). This language can be directl; used by a programmer, and a procedure, extraction, allows one to translate CIC programs into more widely used languages such as OCaml, Haskell or Scheme. Extraction is not a mere syntax change: the type System of CIC is very rich, but purely logical entities can appear inside programs, impacting their performance. Extraction erases these logical artefacts as well. In this thesis, we tackle certification of the extraction itself. We have proved its correction in the context of a full formalization of Coq in Coq. Even though this formalization is not exactly Coq, we worked on it with the concrete implementation of Coq in mind. We also propose a new way to certify extracted programs, in the concrete setting of the existing Coq System

Gli stili APA, Harvard, Vancouver, ISO e altri

45

Ziliani, Beta [Verfasser], e Derek [Akademischer Betreuer] Dreyer. "Interactive typed tactic programming in the Coq proof assistant / Beta Ziliani. Betreuer: Derek Dreyer". Saarbrücken : Saarländische Universitäts- und Landesbibliothek, 2015. http://d-nb.info/1069289868/34.

Testo completo

Gli stili APA, Harvard, Vancouver, ISO e altri

46

Soubiran, Elie. "Développement modulaire de théories et gestion de l'espace de nom pour l'assistant de preuve Coq". Phd thesis, Ecole Polytechnique X, 2010. http://tel.archives-ouvertes.fr/tel-00679201.

Testo completo

Gli stili APA, Harvard, Vancouver, ISO e altri

47

Letouzey, Pierre. "Programmation fonctionnelle certifiée : L'extraction de programmes dans l'assistant Coq". Phd thesis, Université Paris Sud - Paris XI, 2004. http://tel.archives-ouvertes.fr/tel-00150912.

Testo completo

Abstract (sommario):

Nous nous intéressons ici à la génération de programmes certifiés
corrects par construction. Ces programmes sont obtenus en
extrayant l'information pertinente de preuves constructives réalisées
dans l'assistant de preuves Coq.

Une telle traduction, ou "extraction", des preuves constructives
en programmes fonctionnels n'est pas nouvelle, elle correspond
à un isomorphisme bien connu sous le nom de Curry-Howard. Et
l'assistant Coq comporte depuis longtemps un tel outil d'extraction.
Mais l'outil précédent présentait d'importantes limitations. Certaines
preuves Coq étaient ainsi hors de son champ d'application, alors que
d'autres engendraient des programmes incorrects.

Afin de résoudre ces limitations, nous avons effectué une refonte
complète de l'extraction dans Coq, tant du point de vue de la théorie
que de l'implantation. Au niveau théorique, cette refonte a entraîné
la réalisation de nouvelles preuves de correction de ce mécanisme
d'extraction, preuves à la fois complexes et originales. Concernant
l'implantation, nous nous sommes efforcés d'engendrer du code
extrait efficace et réaliste, pouvant en particulier être intégré dans des
développement logiciels de plus grande échelle, par le biais de
modules et d'interfaces.

Enfin, nous présentons également plusieurs études de cas illustrant
les possibilités de notre nouvelle extraction. Nous décrivons ainsi la
certification d'une bibliothèque modulaire d'ensembles finis, et
l'obtention de programmes d'arithmétique réelle exacte à partir d'une
formalisation d'analyse réelle constructive. Même si des progrès
restent encore à obtenir, surtout dans ce dernier cas, ces exemples
mettent en évidence le chemin déjà parcouru.

Gli stili APA, Harvard, Vancouver, ISO e altri

48

Walukiewicz-Chrzaszcz, Daria. "Terminaison de la réécriture dans le calcul des constructions". Paris 11, 2003. http://www.theses.fr/2003PA112050.

Testo completo

Abstract (sommario):

Le sujet de la thèse porte sur la normalisation forte de la réécriture sur les termes du calcul des constructions. Plus précisément, on construit un critère de terminaison décidable, dit HORPO (Higher Order Recursive Path Ordering), sur des règles de réécriture d'ordre supérieur. On prouve que le calcul des constructions enrichi par tout système de règles vérifiant ce critère admet seulement des réductions finies. En même temps on montre que HORPO est suffisamment général pour accepter un grand nombre de définitions de fonctions rencontrées dans la littérature. Ce sujet fait partie de la recherche sur la réécriture d'ordre supérieur et de la recherche sur des extensions du calcul des constructions. Du coté pratique ce sujet de recherche est motivé par le développement des assistants à la démonstration basés sur le calcul des constructions tels que Coq. Les règles de réécriture considérées peuvent être définies sur des symboles de fonctions d'ordre supérieur dont le type peut être dépendant, mais pas sur les constructeurs de types {on ne s'intéresse pas à la réécriture sur les types). Les réductions considérées sont des pas de réécriture et de beta-réduction librement intercalés. La normalisation forte du calcul de constructions avec de la réécriture est prouvée en utilisant les candidats de réductibilité de Girard dans leur version typée proposée par Coquand et Gallier. On montre aussi la propriété de subject réduction, qui est assez compliquée à cause de la non-confluence de HORPO. Mis à part la convertibilité (le coût de vérification de la beta-égalité) l'algorithme pour vérifier si une règle satisfait HORPO est polynomial. La décidabilité et la complexité relativement basse de HORPO sont des arguments importants pour traiter HORPO comme une base pour l'incorporation de réécriture dans un assistant de preuve comme Coq
We show how to incorporate rewriting into the Calculus of Constructions and prove that the resulting system is strongly normalizing with respect to beta and rewrite reductions. More precisely, we present a decidable criterion called HORPO (Higher Order Recursive Path Ordering) on rewrite rules and we show that in the Calculus of Constructions extended by any set of rules satisfying HORPO all reductions are finite. Our criterion is general enough to accept definitions by rewriting of many well-known, higher order functions, for example dependent recursors for inductive types or proof carrying functions. The subject of the thesis is concerned both with the research on the higher-order rewriting and on interesting extensions of the Calculus of Constructions. A practical motivation of this work is the perspective of extending the proof assistants based on the Calculus of Constructions, with a rewriting mechanism. In the thesis the rewrite rules can be defined over higher-order dependently typed function symbols, that are not type-constructors (rewriting on types is out of the scope). Moreover, the rules have to be parametric, which roughly means that all type arguments have to be distinct variables. Reductions consist of arbitrary sequences of rewriting steps and beta-reductions. The strong normalization of the Calculus of Constructions with HORPO is proved using a typed version of Girard's reducibility candidates method, proposed by Coquand and Gallier. The system has the subject reduction property, but its proof is complex since the rewrite relation generated by HORPO is not confluent. Putting aside the convertibility tests (i. E. Beta-equality), checking a rewrite rule has polynomial complexity. Decidability and relatively low complexity of HORPO provide an important argument for considering HORPO as a basis for the incorporation of rewriting in interactive theorem proved based on the Curry-Howard isomorphism, such as Cog

Gli stili APA, Harvard, Vancouver, ISO e altri

49

Spiwack, Arnaud. "Verified computing in homological algebra". Palaiseau, Ecole polytechnique, 2011. http://pastel.archives-ouvertes.fr/docs/00/60/58/36/PDF/thesis.spiwack.pdf.

Testo completo

Abstract (sommario):

L'objet de cette thèse est d'étudier les capacités du système Coq à mélanger démonstrations et programmes en pratique en essayant d'y implémenter une part du programme Kenzo, un outil de calcul formel en algèbre homologique. À cet effet, nous travaillons sous trois contrainte: nous voulons essayer de lire le programme comme une démonstration avec un contenu calculatoire, ces démonstrations doivent calculer efficacement et nous cherchons à éviter de dupliquer des morceaux de démonstration. Nous montrons dans un premier temps comment le soucis d'efficacité conduit à reconsidérer certains aspects des mathématiques traditionnelle. Nous proposons une abstraction catégorielle adaptée, qui répond à la fois à un soucis de clareté et au besoin de partager les démonstration quand c'est possible. Cette abstraction, bien que différente des propositions traditionnelles, permet de formuler les notions d'algèbre homologique dans un style proche de celui de Kenzo. Nous proposons par ailleurs des modifications au programme de Coq pour rendre les démonstrations plus confortables, et pour permettre d'écrire des programmes plus efficaces. La première modification permet d'utiliser des tactiques plus fines, souvent nécessaire quand l'utilisation des types dépendents se fait commune. La seconde permet d'utiliser les capacité du processeur pour faire des calculs plus efficaces sur des entiers. Pour finir nous proposons quelques pistes pour améliorer le partage et la clareté du code. Malheureusement, nous nous heurtons aux limites du système. Nous montrons ainsi que Coq ne tiens pas forcément ses promesses et qu'il y aura besoin de travaux théoriques pour comprendre comment lever ces limites
The object of this thesis is the study of the ability of the Coq system to mix proofs and programs in practice. Our approach consists in implementing part of the program Kenzo, a computer algebra tool for homological algebra under some constraint. We want to be able to read the program as a proof with a computational content, these proofs much compute efficiently, and we try to avoid duplication of proofs or part thereof. We show, first, how the requirement of efficiency leads to revise some aspects of traditional mathematics. We propose a suitable categorical abstraction, both for clarity and to avoid duplications. This abstraction, though different from what is customary in mathematics, allow to formulate the constructs of homological algebra in a style much like that of Kenzo. We propose, then, modifications to the Coq programm. A first one to make proofs more convenient, by allowing the use of more fine grain tactics which are often necessary when dependent types are common. The second modification to leverage the arithmetical abilities of the processor to compute more efficiently on integers. Finally, we propose some leads to improve both sharing and clarity of the proofs. Unfortunately, they push the system beyond its limits. Hence, we show that Coq is not always up to its promises and that theoretical works will be necessary to understand how these limits can be relaxed

Gli stili APA, Harvard, Vancouver, ISO e altri

50

Cano, Guillaume. "Interaction entre algèbre linéaire et analyse en formalisation des mathématiques". Phd thesis, Université Nice Sophia Antipolis, 2014. http://tel.archives-ouvertes.fr/tel-00986283.

Testo completo

Abstract (sommario):

Dans cette thèse nous présentons la formalisation de trois résultats principaux que sont la forme normale de Jordan d'une matrice, le théorème de Bolzano-Weierstraß et le théorème de Perron-Frobenius. Pour la formalisation de la forme normale de Jordan nous introduisons différents concepts d'algèbre linéaire tel que les matrices diagonales par blocs, les matrices compagnes, les facteurs invariants, ... Ensuite nous définissons et développons une théorie sur les espaces topologiques et métriques pour la formalisation du théorème de Bolzano-Weierstraß. La formalisation du théorème de Perron-Frobenius n'est pas terminée. La preuve de ce théorème utilise des résultats d'algèbre linéaire, mais aussi de topologie. Nous montrerons comment les précédents résultats seront réutilisés.

Gli stili APA, Harvard, Vancouver, ISO e altri

Tesi sul tema "Coq (assistant de preuve)"

Cita una fonte nei formati APA, MLA, Chicago, Harvard e in molti altri stili