Verifying Time Complexity of Binary Search using Dafny
Software Engineering
2021-08-09 v1
Abstract
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.
Cite
@article{arxiv.2108.02966,
title = {Verifying Time Complexity of Binary Search using Dafny},
author = {Shiri Morshtein and Ran Ettinger and Shmuel Tyszberowicz},
journal= {arXiv preprint arXiv:2108.02966},
year = {2021}
}
Comments
In Proceedings F-IDE 2021, arXiv:2108.02369