Higher-order constrained horn clauses for verification

Toby Cathcart Burn, Luke Ong, Steven Ramsay

Research output: Contribution to journalArticle (Academic Journal)peer-review

545 Downloads (Pure)

Abstract

Motivated by applications in automated verification of higher-order functional programs, we develop a notion of constrained Horn clauses in higher-order logic and a decision problem concerning their satisfiability. We show that, although satisfiable systems of higher-order clauses do not generally have least models, there is a notion of canonical model obtained through a reduction to a problem concerning a kind of monotone logic program. Following work in higher-order program verification, we develop a refinement type system in order to reason about and automate the search for models. This provides a sound but incomplete method for solving the decision problem. Finally, we show that there is a sense in which we can use refinement types to express properties of terms whilst staying within the higher-order constrained Horn clause framework.
Original languageEnglish
Article number11
Number of pages28
JournalProceedings of the ACM on Programming Languages
Volume2
Issue numberPOPL
Early online date27 Dec 2017
DOIs
Publication statusPublished - 1 Jan 2018

Structured keywords

  • Programming Languages

Fingerprint Dive into the research topics of 'Higher-order constrained horn clauses for verification'. Together they form a unique fingerprint.

Cite this