Advertisement
Published in:
2012 | OriginalPaper | Chapter
Introduction to the Coq Proof-Assistant for Practical Software Verification
Author : Christine Paulin-Mohring
Published in: Tools for Practical Software Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
This paper is a tutorial on using the
Coq
proof-assistant for reasoning on software correctness. It illustrates features of
Coq
like inductive definitions and proof automation on a few examples including arithmetic, algorithms on functional and imperative lists and cryptographic protocols.
Coq
is not a tool dedicated to software verification but a general purpose environment for developing mathematical proofs. However, it is based on a powerful language including basic functional programming and high-level specifications. As such it offers modern ways to literally program proofs in a structured way with advanced data-types, proofs by computation, and general purpose libraries of definitions and lemmas.
Coq
is well suited for software verification of programs involving advanced specifications like language semantics and real numbers. The
Coq
architecture is also based on a small trusted kernel, making possible to use third-party libraries while being sure that proofs are not compromised.