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.

Nous proposons deux caractérisations des arbres réguliers. La première est sémantique et s'appuie sur les types co-inductifs. La seconde est syntaxique et repose sur une représentation des arbres réguliers par des termes cycliques. Nous prouvons que ces deux caractérisations sont isomorphes.Ensuite, nous étudions le problème de la définition de morphisme d'arbres préservant la propriété de régularité. Nous montrons en utilisant le formalisme des transducteurs d'arbres, l'existence d'un critère syntaxique garantissant la préservation de cette propriété. Enfin, nous considérons des applications de la théorie des arbres réguliers comme la définition de l'opérateur de composition parallèle d'une algèbre de processus ou encore, les problèmes de décidabilité sur les arbres réguliers via une mécanisation d'un vérificateur de modèles pour un mu-calcul coalgébrique. Tous les résultats ont été mécanisés et prouvés corrects dans l'assistant de preuve Coq. / We propose two characterizations of regular trees. The first one is semantic and is based on coinductive types. The second one is syntactic and represents regular trees by means of cyclic terms. We prove that both of these characterizations are isomorphic. Then, we study the problem of defining tree morphisms preserving the regularity property. We show, by using the formalism of tree transducers, the existence of syntactic criterion ensuring that this property is preserved. Finally, we consider applications of the theory of regular trees such as the definition of the parallel composition operator of a process algebra or, the decidability problems on regular trees through a mechanization of a model-checker for a coalgebraic mu-calculus. All the results were mechanized and proved correct in the Coq proof assistant.

Ce mémoire présente l'implémentation d'un nouveau langage de programmation nommé Typer. Typer est un langage fonctionnel orienté vers la méta programmation. Il a été conçu pour augmenter la productivité du programmeur et lui permettre d'écrire des applications plus fiables grâce à son système de types. Pour arriver à ses fins, Typer utilise l'inférence de types et implémente un puissant système de macros. L'inférence de types permet à l'utilisateur d'omettre certains éléments, le système de macros, quant à lui, permet de compléter le programme pendant la compilation lorsque l'inférence n'est pas suffisante ou pour générer du code. Typer utilise les types dépendants pour permettre à l'utilisateur de créer des types très expressifs pouvant même être utilisés pour représenter des preuves formelles. De plus, l'expressivité des types dépendants permet au compilateur d'effectuer des vérifications plus approfondies pendant la compilation même. Ces mécaniques permettent au code source d'être moins verbeux, plus concis et plus simple à comprendre, rendant, ainsi l'écriture de programmes ou/et de preuves plus plaisante. Ces fonctionnalités sont implémentées dans l'étape que nous appelons l'élaboration, à l'intérieur de laquelle de nombreuses transformations du code source ont lieu. Ces transformations incluent l'élimination des aides syntaxiques, la résolution des identificateurs, l'expansion des macros, la propagation et l'inférence des types. / This dissertation present the implementation of a new programming language named Typer Typer is a functional programming language oriented towards meta programming. It has been created to increase the programmer productivity and enable him to write safer programs thanks to his type system. To achieve his goal, Typer use type inference and a powerful macro system. Type inference enable to user to elide some elements while the macro system enable us to complete the program during compilation. Typer use dependent type which enable the user to create very expressive types which can even be used to represent formal proofs. Furthermore, dependent type's expressivity enable the compiler to perform a in-depth checks during compilation. Those mechanics enable the source code to be less verbose, shorter and easier to understand, making the writing of new programmes more enjoyable. Those functionalities are implemented during the step we call the elaboration in which numerous transformations occur. Those transformations include the removal of syntactic sugar, identifier resolution, macro expansion and the propagation and the inference of types.

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.

Cette thèse s'inscrit dans le domaine de la vérification dulogiciel. Le but de la vérification du logiciel est d'assurer qu'uneimplémentation, un programme, répond aux exigences, satisfait saspécification. Cela est particulièrement important pour le logicielcritique, tel que des systèmes de contrôle d'avions, trains oucentrales électriques, où un mauvais fonctionnement pendantl'opération aurait des conséquences catastrophiques.Les exigences du logiciel peuvent concerner la sûreté ou lefonctionnement. Les exigences de sûreté, tel que l'absence d'accès à lamémoire en dehors des bornes valides, sont souvent implicites, dans lesens que toute implémentation est censée être sûre. D'autre part, les exigences fonctionnelles spécifient ce que leprogramme est censé faire. La spécification d'un programme est souventexprimée informellement en décrivant en anglais la mission d'une partie du code source. La vérification duprogramme se fait alors habituellement par relecture manuelle,simulation et tests approfondis. Par contre, ces méthodes negarantissent pas que tous les possibles cas d'exécution sontcapturés. La preuve déductive de programme est une méthode complète pour assurerla correction du programme. Ici, un programme, ainsi que saspécification formalisée à l'aide d'un langage logique, est un objetmathématique et ses propriétés désirées sont des théorèmes logiques àprouver formellement. De cette façon, si le système logiquesous-jacent est cohérent, on peut être complètement sûr que lapropriété prouvée est valide pour le programme en question et pourn'importe quel cas d'exécution. La génération de conditions de vérification est une techniquecensée aider le programmeur à prouver les propriétés qu'il veut surson programme. Ici, un outil (VCG) analyse un programme donné avec saspécification et produit une formule mathématique, dont la validitéimplique la correction du programme vis à vis de saspécification, ce qui est particulièrement intéressant lorsque lesformules générées peuvent être prouvées automatiquement à l'aide desolveurs SMT. Cette approche, basée sur des travaux de Hoare et Dijkstra,est bien comprise et prouvée correcte en théorie. Des outils devérification déductive ont aujourd'hui acquis une maturité qui leurpermet d'être appliqués dans un contexte industriel où un hautniveau d'assurance est requis. Mais leurs implémentations doiventgérer toute sorte de fonctionnalités des langages et peuvent donc devenir très complexes et contenir des erreurs ellesmêmes - au pire des cas affirmer qu'un programme est correct alorsqu'il ne l'est pas. Il se pose donc la question du niveau de confianceaccordée à ces outils.Le but de cette thèse est de répondre à cette question. Ondéveloppe et certifie, dans le système Coq, un VCGpour des programmes C annotés avec ACSL, le langage logique pour laspécification de programmes ANSI/ISO C.Notre première contribution est la formalisation d'un VCGexécutable pour le langage intermédiaire Whycert, un langageimpératif avec boucles, exceptions et fonctions récursives, ainsi quesa preuve de correction par rapport à la sémantique opérationnelle bloquante à grand pas du langage. Une deuxièmecontribution est la formalisation du langage logique ACSL et lasémantique des annotations ACSL dans Clight de Compcert. De lacompilation de programmes C annotés vers des programmes Whycert et sapreuve de préservation de la sémantique combiné avec uneaxiomatisation en Whycert du modèle mémoire Compcert résulte notrecontribution principale: une chaîne intégrée certifiée pour lavérification de programmes C, basée sur Compcert. En combinant notrerésultat de correction avec celui de Compcert, on obtient un théorèmeen Coq qui met en relation la validité des l'obligations de preuvegénérées avec la sûreté du code assembleur compilé. / 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.

Les activités de validation et vérification de modèles sont devenues essentielles dans le développement de systèmes complexes. Les efforts de formalisation de ces activités se sont multipliés récemment étant donné leur importance pour les systèmes embarqués critiques. Notre travail s’inscrit principalement dans cette voie. Nous abordons deux visions complémentaires pour traiter cette problématique. La première est une description syntaxique implicite macroscopique basée sur une ontologie pour aider les concepteurs dans le choix des outils selon leurs exigences. La seconde est une description sémantique explicite microscopique pour faciliter la construction de techniques de vérification compositionnelles. Nous proposons dans la première partie de cette thèse une ontologie pour expliquer et expliciter les éléments fondateurs du domaine que nous appelons VVO. Cette ontologie pourra avoir plusieurs autres utilisations : une base de connaissance, un outil de formation ou aussi un support pour le choix de la méthode à appliquer et l’inférence de correspondance entre outils. Nous nous intéressons dans la seconde partie de cette thèse à une formalisation dans un assistant à la preuve de l’introduction de composants dans un langage de modélisation et des liens avec les activités de validation et vérification. Le but est d’étudier la préservation des propriétés par composition : les activités de vérification sont généralement coûteuses en terme de temps et d’effort, les faire d’une façon compositionnelle est très avantageux. Nous partons de l’atelier formel pour l’Ingénierie Dirigée par les Modèles Coq4MDE. Nous suivons la même ligne directrice de développement prouvé pour formaliser des opérateurs de composition et étudier la conservation des propriétés par assemblage. Nous nous intéressons au typage puis à la conformité de modèles par rapport au métamodèle et nous vérifions que les opérateurs définis permettent de conserver ces propriétés. Nous nous focalisons sur l’étude d’opérateurs élémentaires que nous exploitons pour spécifier des opérateurs de plus haut niveau. Les préconditions des opérateurs représentent les activités de vérification non compositionnelles qui doivent être effectuées en plus de la vérification des composants pour assurer la postcondition des opérateurs qui est la propriété souhaitée. Nous concluons en présentant des perspectives pour une formalisation algébrique en théorie des catégories. / The validation and verification of models have become essential in the development of complex systems. The formalisation efforts for these activities have increased recently being given their importance for critical embedded systems. We discuss two complementary visions for addressing these issues. The first is a syntactic implicit macroscopic description based on an ontology to help designers in the choice of tools depending on their requirements. The second is a microscopic explicit semantics description aiming to facilitate the construction of compositional verification techniques. We propose in the first part of this thesis an ontology to explain and clarify the basic elements of the domain of Verification and Validation that we call VVO. This ontology may have several other uses: a knowledge base, a training tool or a support for the choice of the method to be applied and to infer correspondence between tools. We are interested in the second part of this thesis in a formalisation using a proof assistant for the introduction of components in a modelling language and their links with verification and validation activities. The aim is to study the preservation of properties by the composition activities. The verification are generally expensive in terms of time and efforts, making theme in a compositional way is very advantageous. Starting from the formal framework for Model Driven Engineering COQ4MDE, we follow the same line of though to formalize the composition operators and to study the conservation of properties by composition. We are interested in typing and conformity of models in relation with metamodels and we verify that the defined operators allow to preserve these properties. We focus on the study of elementary operators that we use to specify hight level operators. The preconditions for the operators represent the non-compositional verification activities that should be performed in addition to verification of components to ensure the desired postcondition of the operator. We conclude by studying algebraic formalisation using concepts from category theory.

Made available in DSpace on 2015-03-03T15:47:47Z (GMT). No. of bitstreams: 1 PatrickCAT_DISSERT.pdf: 4794202 bytes, checksum: 05088b21ff2be2b3c2ccec958e7e6b62 (MD5) Previous issue date: 2013-06-03 / Logic courses represent a pedagogical challenge and the recorded number of cases of failures and of discontinuity in them is often high. Amont other difficulties, students face a cognitive overload to understand logical concepts in a relevant way. On that track, computational tools for learning are resources that help both in alleviating the cognitive overload scenarios and in allowing for the practical experimenting with theoretical concepts. The present study proposes an interactive tutorial, namely the TryLogic, aimed at teaching to solve logical conjectures either by proofs or refutations. The tool was developed from the architecture of the tool TryOcaml, through support of the communication of the web interface ProofWeb in accessing the proof assistant Coq. The goals of TryLogic are: (1) presenting a set of lessons for applying heuristic strategies in solving problems set in Propositional Logic; (2) stepwise organizing the exposition of concepts related to Natural Deduction and to Propositional Semantics in sequential steps; (3) providing interactive tasks to the students. The present study also aims at: presenting our implementation of a formal system for refutation; describing the integration of our infrastructure with the Virtual Learning Environment Moodle through the IMS Learning Tools Interoperability specification; presenting the Conjecture Generator that works for the tasks involving proving and refuting; and, finally to evaluate the learning experience of Logic students through the application of the conjecture solving task associated to the use of the TryLogic / A disciplina de L?gica representa um desa o tanto para docentes como para discentes, o que em muitos casos resulta em reprova??es e desist?ncias. Dentre as dificuldades enfrentadas pelos alunos est? a sobrecarga da capacidade cognitiva para compreender os conceitos l?gicos de forma relevante. Neste sentido, as ferramentas computacionais de aprendizagem s?o recursos que auxiliam a redu??o de cen?rios de sobrecarga cognitiva, como tamb?m permitem a experi?ncia pr?tica de conceitos te?ricos. O presente trabalho prop?e uma tutorial interativo chamado TryLogic, visando ao ensino da tarefa de Demonstra??o ou Refuta??o (DxR) de conjecturas l?gicas. Trata-se de uma ferramenta desenvolvida a partir da arquitetura do TryOcaml atrav?s do suporte de comunica??o da interface web ProofWeb para acessar o assistente de demonstra??o de teoremas Coq. Os objetivos do TryLogic s?o: (1) Apresentar um conjunto de li??es para aplicar estrat?gias heur?sticas de an?lise de problemas em L?gica Proposicional; (2) Organizar em passo-a-passo a exposi ??o dos conte?dos de Dedu??o Natural e Sem?ntica Proposicional de forma sequencial; e (3) Fornecer aos alunos tarefas interativas. O presente trabalho prop?e tamb?m apresentar a nossa implementa??o de um sistema formal de refuta??o; descrever a integra??o de nossa infraestrutura com o Ambiente Virtual de Aprendizagem Moodle atrav?s da especi ca??o IMS Learning Tools Interoperability ; apresentar o Gerador de Conjecturas de tarefas de Demonstra??o e Refuta??o e, por m, avaliar a experi?ncia da aprendizagem de alunos de L?gica atrav?s da aplica??o da tarefa de DxR em associa??o ? utiliza??o do TryLogic

Eine Herausforderung der Softwareentwicklung ist, die Korrektheit einer Software sicherzustellen. Testen bietet es keine mathematische Korrektheit. Formale Verifikation ist jedoch oft zu aufwändig. Laufzeitverifikation steht zwischen den beiden Methoden. Laufzeitverifikation beantwortet die Frage, ob ein Eingabe-Ausgabe-Paar korrekt ist. Ein zertifizierender Algorithmus überzeugt seinen Nutzer durch ein Korrektheitsargument zur Laufzeit. Dafür berechnet ein zertifizierender Algorithmus für eine Eingabe zusätzlich zur Ausgabe noch einen Zeugen – ein Korrektheitsargument. Jeder zertifizierende Algorithmus besitzt ein Zeugenprädikat: Ist dieses erfüllt für eine Eingabe, eine Ausgabe und einen Zeugen, so ist das Eingabe-Ausgabe-Paar korrekt. Ein simpler Algorithmus, der das Zeugenprädikat für den Nutzer entscheidet, ist ein Checker. Die Korrektheit des Checkers ist folglich notwendig für den Ansatz und die formale Instanzverifikation, bei der wir Checker verifizieren und einen maschinen-geprüften Beweis für die Korrektheit eines Eingabe-Ausgabe-Paars zur Laufzeit gewinnen. Zertifizierende sequentielle Algorithmen sind gut untersucht. Verteilte Algorithmen, die auf verteilten Systemen laufen, unterscheiden sich grundlegend von sequentiellen Algorithmen: die Ausgabe ist über das System verteilt oder der Algorithmus läuft fortwährend. Wir untersuchen zertifizierende verteilte Algorithmen. Unsere Forschungsfrage ist: Wie können wir das Konzept zertifizierender sequentieller Algorithmen so auf verteilte Algorithmen übertragen, dass wir einerseits nah am ursprünglichen Konzept bleiben und andererseits die Gegebenheiten verteilter Systeme berücksichtigen? Wir stellen eine Methode der Übertragung vor. Die beiden Ziele abwägend entwickeln wir eine Klasse zertifizierender verteilter Algorithmen, die verteilte Zeugen berechnen und verteilte Checker besitzen. Wir präsentieren Fallstudien, Entwurfsmuster und ein Framework zur formalen Instanzverifikation. / A major problem in software engineering is to ensure the correctness of software. Testing offers no mathematical correctness. Formal verification is often too costly. Runtime verification stands between the two methods. Runtime verification answers the question whether an input-output pair is correct. A certifying algorithm convinces its user at runtime by offering a correctness argument. For each input, a certifying algorithm computes an output and additionally a witness. Each certifying algorithm has a witness predicate – a predicate with the property: being satisfied for an input, output and witness implies the input-output pair is correct. A simple algorithm deciding the witness predicate for the user is a checker. Hence, the checker’s correctness is crucial to the approach and motivates formal instance verification where we verify checkers and obtain machine-checked proofs for the correctness of an input-output pair at runtime. Certifying sequential algorithms are well-established. Distributed algorithms, designed to run on distributed systems, behave fundamentally different from sequential algorithms: their output is distributed over the system or they even run continuously. We investigate certifying distributed algorithms. Our research question is: How can we transfer the concept of certifying sequential algorithms to distributed algorithms such that we are in line with the original concept but also adapt to the conditions of distributed systems? In this thesis, we present a method to transfer the concept: Weighing up both sometimes conflicting goals, we develop a class of certifying distributed algorithms that compute distributed witnesses and have distributed checkers. We offer case studies, design patterns and a framework for formal instance verification. Additionally, we investigate other methods to transfer the concept of certifying algorithms to distributed algorithms.

Dependent type theories are a kind of mathematical foundations investigated both for the formalisation of mathematics and for reasoning about programs. They are implemented as the kernel of many proof assistants and programming languages with proofs (Coq, Agda, Idris, Dedukti, Matita, etc). Dependent types allow to encode elegantly and constructively the universal and existential quantifications of higher-order logics and are therefore adapted for writing logical propositions and proofs. However, their usage is not limited to the area of pure logic. Indeed, some recent work has shown that they can also be powerful for driving the construction of programs. Using more precise types not only helps to gain confidence about the program built, but it can also help its construction, giving rise to a new style of programming called Type-Driven Development. However, one difficulty with reasoning and programming with dependent types is that proof obligations arise naturally once programs become even moderately sized. For example, implementing an adder for binary numbers indexed over their natural number equivalents naturally leads to proof obligations for equalities of expressions over natural numbers. The need for these equality proofs comes, in intensional type theories (like CIC and ML) from the fact that in a non-empty context, the propositional equality allows us to prove as equal (with the induction principles) terms that are not judgementally equal, which implies that the typechecker can't always obtain equality proofs by reduction. As far as possible, we would like to solve such proof obligations automatically, and we absolutely need it if we want dependent types to be use more broadly, and perhaps one day to become the standard in functional programming. In this thesis, we show one way to automate these proofs by reflection in the dependently typed programming language Idris. However, the method that we follow is independent from the language being used, and this work could be reproduced in any dependently-typed language. We present an original type-safe reflection mechanism, where reflected terms are indexed by the original Idris expression that they represent, and show how it allows us to easily construct and manipulate proofs. We build a hierarchy of correct-by-construction tactics for proving equivalences in semi-groups, monoids, commutative monoids, groups, commutative groups, semi-rings and rings. We also show how each tactic reuses those from simpler structures, thus avoiding duplication of code and proofs. Finally, and as a conclusion, we discuss the trust we can have in such machine-checked proofs.

La mémoire transactionnelle est un mécanisme de plus en plus populaire pour la programmation parallèle et concurrente. Dans la plupart des implantations, l’emboîtement de transactions n’est pas possible ce qui pénalise la modularité. Plutôt que les transactions, qui sont un choix possible d’implantation, nous considérons directement la notion de section atomique. Dans un objectif d’améliorer la modularité et l’expressivité, nous considérons un langage impératif simple étendu avec des instructions de parallélisme avec lancement et attente de processus légers et une instruction de section atomique à portée syntaxique, depuis laquelle des processus légers peuvent s’échapper. Dans ce contexte notre première contribution est la définition précise de l’atomicité et de la bonne synchronisation. Nous prouvons que pour des traces bien formées, la dernière implique la forme forte de la première. Ceci est fait sur des traces d’exécution abstraites dans le sens où nous ne définissons par précisément la syntaxe et la sémantique opérationnelle d’un langage de programmation. Cette première partie de notre travail peut être considérée comme une spécification pour un tel langage. Nous avons utilisé l’assistant de preuve Coq pour modéliser et prouver nos résultats. Notre deuxième contribution est la définition formelle du langage Atomic Fork Join (AFJ). Nous montrons que les traces de sa sémantique opérationnelle vérifient effectivement les conditions de bonne formation définies précédemment. La troisième contribution est la compilation de programmes AFJ en programmes Lock Unlock Fork Join (LUFJ) un langage avec processus léger et verrous mais sans sections atomiques. Nous étudions la correction de la compilation de AFJ vers LUFJ. / Transactions are becoming a popular mechanism for parallel and concurrent programming. In most implementations the nesting of transactions is not supported which hinders modularity. Rather than transactions, which are an implementation choice, we consider directly the notion of atomic section. For the sake of modularity with we consider a simple imperative language with fork/join parallelism and lexically scoped nested atomic sections from which threads can escape. In this context, our first contribution is the precise definition of atomicity, well-synchronisation and the proof that the latter implies the strong form of the former. This is done on execution traces without being specific to a language syntax and operational semantics. This first part of our work could be considered as a specification for the design and implementation of such a parallel language. A formalisation of our results in the Coq proof assistant is also available. Our second contribution is a formal definition of the Atomic Fork Join (AFJ) language and its operational semantics. We show that it indeed satisfies the conditions previously defined. The third contribution of our work is a compilation procedure of AFJ programs to programs another language with threads and locks but without atomic sections, named Lock Unlock Fork Join (LUFJ). We study the correctness of the compilation from AFJ to LUFJ.