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 List.fold.

Litao Zhou (Tony)
Litao Zhou (Tony)
Senior undegraduate

Senior computer science undergraduate at SJTU, interested in PL.

Related