Imperial College London
Alternate

ProfessorSophiaDrossopoulou

Faculty of Engineering, Department of Computing

Professor of Programming Languages
 
 
 
//

Contact

 

s.drossopoulou Website

 
 
//

Location

 

559Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inbook{Certezeanu:2016:10.1007/978-3-319-30734-3_27,
author = {Certezeanu, R and Drossopoulou, S and Egelund-Muller, B and Leino, KRM and Sivarajan, S and Wheelhouse, M},
booktitle = {Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boeron the Occasion of His 60th Birthday},
doi = {10.1007/978-3-319-30734-3_27},
pages = {407--426},
publisher = {Springer International Publishing},
title = {Quicksort Revisited: Verifying Alternative Versions of Quicksort},
url = {http://dx.doi.org/10.1007/978-3-319-30734-3_27},
year = {2016}
}
Download

RIS format (EndNote, RefMan)

TY  - CHAP
AB  - 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.
AU  - Certezeanu,R
AU  - Drossopoulou,S
AU  - Egelund-Muller,B
AU  - Leino,KRM
AU  - Sivarajan,S
AU  - Wheelhouse,M
DO  - 10.1007/978-3-319-30734-3_27
EP  - 426
PB  - Springer International Publishing
PY  - 2016///
SN  - 9783319307336
SP  - 407
TI  - Quicksort Revisited: Verifying Alternative Versions of Quicksort
T1  - Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boeron the Occasion of His 60th Birthday
UR  - http://dx.doi.org/10.1007/978-3-319-30734-3_27
UR  - http://hdl.handle.net/10044/1/34366
ER  -
Download