Abstract
We verify the correctness of a recursive version of Tony Hoare’s quicksort algorithm using the Hoare-logic based verification tool Dafny. We then develop a non-standard, iterative version which is based on a stack of pivot-locations rather than the standard stack of ranges. We outline an incomplete Dafny proof for the latter.
Author supplied keywords
Cite
CITATION STYLE
Certezeanu, R., Drossopoulou, S., Egelund-Muller, B., Leino, K. R. M., Sivarajan, S., & Wheelhouse, M. (2016). Quicksort revisited verifying alternative versions of quicksort. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9660, pp. 407–426). Springer Verlag. https://doi.org/10.1007/978-3-319-30734-3_27
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
