Skip to Main content Skip to Navigation

Application de la théorie des types et du démonstrateur COQ à la vérification de programmes parallèles

Abstract : This thesis is an approach to the formaI specification and verification of distributed systems and in particular to the computer assisted verification. In this work, we use the COQ prover to verify concurrent programs and the chosen specification mechanism is the UNITY logic. First, we describe the Calculus of Inductive Constructions, which is the logic used in the Coq prover. Then we introduce the UNITY theory, but we linger over the problems of its logic, due to the ambiguity of quantifications in the Hoare triples. We propose also an extension of the logic, which solves these problems: a program's context is introduced and a new definition for reachable states is given. After the correctness and the completness of this new logic, we present the Coq-UNITY tool, which results of the implementation of this extension in the Coq system. To illustrate the feasibility of our approach, we present several examples of different complexities: the euclidian division, the reader-writer, the parking and the lift control. These four examples are the first case studies. Each of them highlights a particular problem either in proofs or in specifications. A last example describes a telecommunication protocol, namely the ABT/DT protocol. This example shows that the context is an important notion. Once the context is well-defined, it becomes very helpful in the verification.
Document type :
File URL :
Complete list of metadatas
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 10:58:04 AM
Last modification on : Friday, February 26, 2021 - 3:26:01 PM


  • HAL Id : tel-01747367, version 1



Barbara Heyd. Application de la théorie des types et du démonstrateur COQ à la vérification de programmes parallèles. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 1997. Français. ⟨NNT : 1997NAN10291⟩. ⟨tel-01747367⟩



Record views