J.-C. Filliātre and N. Magaud. Certification of sorting algorithms in the system Coq. In Theorem Proving in Higher Order Logics: Emerging Trends, 1999.

We present the formal proofs of total correctness of three sorting algorithms in the system Coq, namely insertion sort, quicksort and heapsort. The implementations are imperative programs working in-place on a given array. Those developments demonstrate the usefulness of inductive types and higher-order logic in the process of software certification. They also show that the proof of rather complex algorithms may be done in a small amount of time - only a few days for each development - and without great difficulty.

[ bib | .ps.gz ]

Back