Verifying Time Complexity of Binary Search using Dafny
This work addresses the challenge of inefficient code causing performance issues in large systems, though it is incremental as it applies an existing verification tool to a specific algorithm.
The authors tackled the problem of verifying nonfunctional properties like time complexity, which are typically done manually, by using the Dafny verification tool to specify and prove the worst-case time complexity of binary search, demonstrating a proof of concept that can also aid in teaching algorithms.
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.