Higher-order constrained horn clauses for verification
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 h...
| Glavni autori: | , , |
|---|---|
| Format: | Journal article |
| Jezik: | English |
| Izdano: |
Association for Computing Machinery
2017
|
| _version_ | 1826281144584241152 |
|---|---|
| author | Cathcart Burn, T Ong, C Ramsay, S |
| author_facet | Cathcart Burn, T Ong, C Ramsay, S |
| author_sort | Cathcart Burn, T |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T00:24:23Z |
| format | Journal article |
| id | oxford-uuid:7da12e9a-ea81-4263-99c4-352e63e3cc59 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T00:24:23Z |
| publishDate | 2017 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:7da12e9a-ea81-4263-99c4-352e63e3cc592022-03-26T21:04:53ZHigher-order constrained horn clauses for verificationJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:7da12e9a-ea81-4263-99c4-352e63e3cc59EnglishSymplectic Elements at OxfordAssociation for Computing Machinery2017Cathcart Burn, TOng, CRamsay, SMotivated 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. |
| spellingShingle | Cathcart Burn, T Ong, C Ramsay, S Higher-order constrained horn clauses for verification |
| title | Higher-order constrained horn clauses for verification |
| title_full | Higher-order constrained horn clauses for verification |
| title_fullStr | Higher-order constrained horn clauses for verification |
| title_full_unstemmed | Higher-order constrained horn clauses for verification |
| title_short | Higher-order constrained horn clauses for verification |
| title_sort | higher order constrained horn clauses for verification |
| work_keys_str_mv | AT cathcartburnt higherorderconstrainedhornclausesforverification AT ongc higherorderconstrainedhornclausesforverification AT ramsays higherorderconstrainedhornclausesforverification |