Skip to main content

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

1st March 2020 to 28th February 2023

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. 



Share this: