Quicksort Revisited: Verifying Alternative Versions of Quicksort - Certezeanu,R; Drossopoulou,S; Egelund-Muller,B; Leino,KRM; Sivarajan,S; Wheelhouse,M (Springer International Publishing, 2016)
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.