1. Home
  2. IT
  3. Software technologies and System architectures

  4. Coq, proof assistant

Article | REF: H3310 V1

Coq, proof assistant

Authors: Sandrine Blazy, Pierre Castéran, Hugo Herbelin

Publication date: August 10, 2017 | Lire en français

You do not have access to this resource.
Click here to request your free trial access!

Already subscribed? Log in!

Automatically translated using artificial intelligence technology (Note that only the original version is binding) > find out more.

    A  |  A

    Overview

    ABSTRACT

    A proof assistant is an interactive software program used for semi-automatically building large proofs and verifying their correctness. This kind of tool is particularly useful for certifying critical software. In this article, we present Coq, a proof assistant whose development is coordinated by the Inria research institute. First we use a very simple example: the verification of a sorting function for lists, to show how Coq is used in an interactive session. Second, we present some real applications to software verification and mathematics. Coq is considered one of the most trustworthy tools for software validation. We explain some reasons for its success: its theoretical foundations and its constant evolution for over thirty years.

    Read this article from a comprehensive knowledge base, updated and supplemented with articles reviewed by scientific committees.

    Read the article

    AUTHORS

     INTRODUCTION

    In view of the growing importance of – software and hardware components – in critical areas as diverse as transport, energy, healthcare, finance, etc., the need for safe components is becoming ever more pressing.

    For example, the execution of a program must be error-free under the intended application conditions: absence of runtime errors or unwanted looping, compliance with a functional specification.

    However, since Turing , we have known that no algorithm can automatically take a given program and render a correction diagnosis in a finite amount of time. Consequently, only part of the software certification task can be automated. For the rest, interactive tools can be used, where the often complex –– proof of correctness must be guided by the user.

    Proof assistants are interactive software programs that help users to prove theorems, relieving them...

    You do not have access to this resource.

    Exclusive to subscribers. 97% yet to be discovered!

    You do not have access to this resource.
    Click here to request your free trial access!

    Already subscribed? Log in!

    The Ultimate Scientific and Technical Reference

    A Comprehensive Knowledge Base, with over 1,200 authors and 100 scientific advisors
    + More than 10,000 articles and 1,000 how-to sheets, over 800 new or updated articles every year
    From design to prototyping, right through to industrialization, the reference for securing the development of your industrial projects

    KEYWORDS

    formal method   |   proof assistant   |   logic   |   program proving   |   certified software   |   Coq

    This article is included in

    Software technologies and System architectures

    This offer includes:

    Knowledge Base

    Updated and enriched with articles validated by our scientific committees

    Services

    A set of exclusive tools to complement the resources

    Practical Path

    Operational and didactic, to guarantee the acquisition of transversal skills

    Doc & Quiz

    Interactive articles with quizzes, for constructive reading

    Subscribe now!

    Ongoing reading
    Coq, proof assistant
    Outline