Verifying Time Complexity of Binary Search using Dafny

Shiri Morshtein
(School of Computer Science The Academic College Tel-Aviv Yaffo)
Ran Ettinger
(Department of Computer Science Ben-Gurion University of the Negev)
Shmuel Tyszberowicz
(RISE - Centre for Research and Innovation in Software Engineering, Southwest University, Chongqing, China and Department of Software Engineering, Afeka Academic College of Engineering, Tel Aviv, Israel)

Formal software verification techniques are widely used to specify and prove the functional correctness of programs. However, nonfunctional properties such as time complexity are usually carried out with pen and paper. Inefficient code in terms of time complexity may cause massive performance problems in large-scale complex systems. We present a proof of concept for using the Dafny verification tool to specify and verify the worst-case time complexity of binary search. This approach can also be used for academic purposes as a new way to teach algorithms and complexity.

In José Proença and Andrei Paskevich: Proceedings of the 6th Workshop on Formal Integrated Development Environment (F-IDE 2021), Held online, 24-25th May 2021, Electronic Proceedings in Theoretical Computer Science 338, pp. 68–81.
Published: 6th August 2021.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: