Verification Of Counting Sort And Radix Sort
DEDUCTIVE SOFTWARE VERIFICATION - THE KEY BOOK: FROM THEORY TO PRACTICE(2016)
摘要
textabstractSorting is an important algorithmic task used in many applications. Two main aspects of sorting algorithms which have been studied extensively are complexity and correctness. [Foley and Hoare, 1971] published the first formal correctness proof of a sorting algorithm (Quicksort). While this is a handwritten proof, the development and application of (semi)-automated theorem provers has since taken a huge flight. The major sorting algorithms Insertion sort, Heapsort and Quicksort were proven correct by Filliâtre and Magaud [1999] using the proof assistant Coq. Recently, Sternagel [2013] formalized a proof of Mergesort within the interactive theorem prover Isabelle/HOL.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络