A Tour of Formal Verification with Coq:Knuth's Algorithm for Prime Numbers

Laurent Théry 1
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : In his book "The Art of Computer Programming", Donald Knuth gives an algorithm to compute the first n prime numbers. Surprisingly, proving the correctness of this simple algorithm from basic principles is far from being obvious and requires a wide range of verification techniques. In this paper, we explain how the verification has been mechanized in the Coq proof system.
Document type :
Reports
Complete list of metadatas

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/inria-00071985
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 7:25:08 PM
Last modification on : Thursday, February 14, 2019 - 5:48:01 PM
Long-term archiving on : Sunday, April 4, 2010 - 8:55:00 PM

Identifiers

  • HAL Id : inria-00071985, version 1

Collections

Citation

Laurent Théry. A Tour of Formal Verification with Coq:Knuth's Algorithm for Prime Numbers. RR-4600, INRIA. 2002. ⟨inria-00071985⟩

Share

Metrics

Record views

109

Files downloads

1115