Automatic Verification of Higher Order programs
The goal of this project is to provide a solution to automatic verification of higher order programs and implement a prototype system to verify several concrete examples of higher order programs.
In this project we take a subset language of OCaml, and explore the automatic verification of higher order functions based on the structure of HIP/SLEEK system. We integrate new designs such as abstract predicates and nested function specifications in this project and implement a prototype system by encoding SMT queries to Z3 solver. The system has shown its usefulness in several examples including common higher order functions such as