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...
| Príomhchruthaitheoirí: | , , |
|---|---|
| Formáid: | Journal article |
| Teanga: | English |
| Foilsithe / Cruthaithe: |
Association for Computing Machinery
2017
|