Certification of Insert-Sort and Merge-Sort in Coq

We present the formalization and the automated verification of the list sorting algorithms Insert-Sort and Merge-Sort in the Coq system and we compare it with the formalization and verification of the same algorithms in the Theorema system, which have been performed in our previous work. This represents a case study in verification of complex al-gorithms, sorting being particularly important because it plays a crucial role in various applications that handle large data amounts, as for instance in environmental modelling and re-search. This is part of our research on using Automated Rea-soning - one of the oldest and most important field of Artificial Intelligence - for formal verification of complex systems, whose safe behaviour must be insured, as for instance in robotic systems that interact with people. Concretely, the specification of correctness of these two al-gorithms, as well as the definition of the algorithms are very similar in the two systems, however the proof styles and the number of necessary lemmas are quite different. Coq needs more lemmas and the proof is constructed via a proof script, and the necessary domain properties are imported from Coq libraries. In Theorema the proof is based on domain-specific inferences and strategies, is presented in natural style, and most of the domain specific properties are embedded in the inference rules and proof strategies. However the Theorema system is in principle error prone, because there is no requirement for algorithm termination, for the consistency of inference rules, and for the proof of the properties. In contrast, in Coq everything is rigorously checked, thus it is guarantied to be correct.