A Tour of Formal Verification with Coq:Knuths Algorithm for Prime NumbersReportar como inadecuado




A Tour of Formal Verification with Coq:Knuths Algorithm for Prime Numbers - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

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.

Keywords : PROGRAM VERIFICATION COQ PRIME NUMBERS BERTRAND-S POSTULATE





Autor: Laurent Théry -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados