Higher-order Constrained Horn Clauses: A New Approach to Verifying Higher-order Programs

This project aims to develop a new approach to the verification of higher-order programs based on higher-order constrained Horn-clauses. A recent innovation in symbolic model checking, Horn constraints exploit the successful combination of automated deduction technologies with the satisfiability checking of formulas. Our verification method will be automatic and programming-language independent. 

The project is a collaboration between Oxford and Bristol.