Expressivity and Algorithmics of Higher-Order Horn Clauses
Lead Research Organisation:
University of Oxford
Department Name: Computer Science
Abstract
This project falls within the EPSRC Verification and Correctness research area
Automated program verification is important as it has the potential to reduce the resources required by software development and improve the quality. Higher-order program verification is becoming increasingly important since the use of languages with higher-order features is rising and language versions such as Java 8 and C++11 have added support for higher-order functions.
The project proposes to examine the expressive power of higher-order Horn clauses by comparing them to other formalisms of verification. Specifically, it will investigate how to express modal mu-calculus model checking problems as higher-order Horn clause problems, possibly by extending the syntax of higher-order Horn clauses to allow for the fact that modal mu-calculus allows both least and greatest fixpoint operators. This is expected to lead to algorithms for generating systems of higher-order Horn clauses from existing program verification problems.
Higher-order Horn Clauses have been investigated for the purposes of logic programming, but only recently as a tool for program verification, so there is much about them not currently known, and this pursues an original direction of research. First-order Horn clauses have been used as an intermediate format in program verification between translation and solving. This enables solving techniques to be more easily extended to many programming languages and means that a particular translator can be used with existing and future solvers thanks to separation of concerns. It also allows intermediate transformation steps that both produce and consume Horn clauses.
However, first-order Horn clauses suffer imprecision when used with higher-order programs since they require working with a first-order approximation to the program's behaviour. Higher-order Horn clauses are a promising area of research since it is possible to use them to express higher-order program verification problems without losing information about the higher-order nature of the programs.
This project would reveal the advantages and limitations of higher-order Horn clauses relative to similar approaches, and could indicate whether they can be as effective in higher-order program verification as first order Horn clauses are for first-order programs. This will then inform and encourage further development of techniques for working with higher-order Horn clauses.
Automated program verification is important as it has the potential to reduce the resources required by software development and improve the quality. Higher-order program verification is becoming increasingly important since the use of languages with higher-order features is rising and language versions such as Java 8 and C++11 have added support for higher-order functions.
The project proposes to examine the expressive power of higher-order Horn clauses by comparing them to other formalisms of verification. Specifically, it will investigate how to express modal mu-calculus model checking problems as higher-order Horn clause problems, possibly by extending the syntax of higher-order Horn clauses to allow for the fact that modal mu-calculus allows both least and greatest fixpoint operators. This is expected to lead to algorithms for generating systems of higher-order Horn clauses from existing program verification problems.
Higher-order Horn Clauses have been investigated for the purposes of logic programming, but only recently as a tool for program verification, so there is much about them not currently known, and this pursues an original direction of research. First-order Horn clauses have been used as an intermediate format in program verification between translation and solving. This enables solving techniques to be more easily extended to many programming languages and means that a particular translator can be used with existing and future solvers thanks to separation of concerns. It also allows intermediate transformation steps that both produce and consume Horn clauses.
However, first-order Horn clauses suffer imprecision when used with higher-order programs since they require working with a first-order approximation to the program's behaviour. Higher-order Horn clauses are a promising area of research since it is possible to use them to express higher-order program verification problems without losing information about the higher-order nature of the programs.
This project would reveal the advantages and limitations of higher-order Horn clauses relative to similar approaches, and could indicate whether they can be as effective in higher-order program verification as first order Horn clauses are for first-order programs. This will then inform and encourage further development of techniques for working with higher-order Horn clauses.
Organisations
People |
ORCID iD |
| Luke Ong (Primary Supervisor) | |
| Toby Cathcart Burn (Student) |
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/N509711/1 | 01/10/2016 | 30/09/2021 | |||
| 1893570 | Studentship | EP/N509711/1 | 01/10/2017 | 31/03/2021 | Toby Cathcart Burn |