Coq, proof assistant

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

Sandrine Blazy: University of Rennes 1, IRiSA, CNRS
Pierre Castéran: Univ. Bordeaux, LaBRI, CNRS, INP Bordeaux
Hugo Herbelin: Researcher Inria Paris

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!

KEYWORDS