Verifying Time Complexity of Binary Search using Dafny. - Shiri Morshtein; Ran Ettinger; Shmuel S. Tyszberowicz (F-IDE@NFM, 2021)