Viper verification of three Challenges Challenge 1: Circular Buffers Challenge 2: Verification of Time Task 1: Basic Runtime Analysis Task 2: Binary Search Trees Task 3: Dynamic Arrays Challenge 3: Morris Algorithm (a tree traversal algorithm that does not employ the use of recursion or a stack)