Misplaced Pages

Constrained Horn clauses

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
Fragment of first-order logic
This article is missing information about if they are named after somebody? When were they first defined? Perhaps add an example?. Please expand the article to include this information. Further details may exist on the talk page. (December 2023)

Constrained Horn clauses (CHCs) are a fragment of first-order logic with applications to program verification and synthesis. Constrained Horn clauses can be seen as a form of constraint logic programming.

Definition

A constrained Horn clause is a formula of the form

ϕ ∧ P 1 ( x 1 ) ∧ … ∧ P n ( x n ) → P ( x ) {\displaystyle \phi \land P_{1}(\mathbf {x} _{1})\land \ldots \land P_{n}(\mathbf {x_{n}} )\to P(\mathbf {x} )}

where ϕ {\displaystyle \phi } is a constraint in some first-order theory, P i {\displaystyle P_{i}} are predicates, and x i {\displaystyle \mathbf {x} _{i}} are universally-quantified variables. The addition of constraint makes it a generalization of the plain Horn clause.

Decidability

The satisfiability of constrained Horn clauses with constraints from linear integer arithmetic is undecidable.

Solvers

There are several automated solvers for CHCs, including the SPACER engine of Z3.

CHC-COMP is an annual competition of CHC solvers. CHC-COMP has run every year since 2018.

Applications

Constrained Horn clauses are a convenient language in which to specify problems in program verification. The SeaHorn verifier for LLVM represents verification conditions as constrained Horn clauses, as does the JayHorn verifier for Java.

References

  1. Angelis, Emanuele De; Fioravanti, Fabio; Gallagher, John P.; Hermenegildo, Manuel V.; Pettorossi, Alberto; Proietti, Maurizio (November 2022). "Analysis and Transformation of Constrained Horn Clauses for Program Verification". Theory and Practice of Logic Programming. 22 (6): 974–1042. arXiv:2108.00739. doi:10.1017/S1471068421000211. ISSN 1471-0684. S2CID 236777105. CHCs are syntactically and semantically the same as constraint logic programs
  2. Cox, Jim; McAloon, Ken; Tretkoff, Carol (1992-06-01). "Computational complexity and constraint logic programming languages". Annals of Mathematics and Artificial Intelligence. 5 (2): 163–189. doi:10.1007/BF01543475. ISSN 1573-7470. S2CID 666608.
  3. Blicha, Martin; Britikov, Konstantin; Sharygina, Natasha (2023). "The Golem Horn Solver". In Enea, Constantin; Lal, Akash (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer Nature Switzerland. pp. 209–223. doi:10.1007/978-3-031-37703-7_10. ISBN 978-3-031-37703-7.
  4. Gurfinkel, Arie (2022). "Program Verification with Constrained Horn Clauses (Invited Paper)". In Shoham, Sharon; Vizel, Yakir (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 13371. Cham: Springer International Publishing. pp. 19–29. doi:10.1007/978-3-031-13185-1_2. ISBN 978-3-031-13185-1.
  5. Fedyukovich, Grigory; Rümmer, Philipp (2021-09-10). "Competition Report: CHC-COMP-21". Electronic Proceedings in Theoretical Computer Science. 344: 91–108. arXiv:2109.04635v1. doi:10.4204/EPTCS.344.7. S2CID 221132231.
  6. Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey (2015), Beklemishev, Lev D.; Blass, Andreas; Dershowitz, Nachum; Finkbeiner, Bernd (eds.), "Horn Clause Solvers for Program Verification", Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, Lecture Notes in Computer Science, Cham: Springer International Publishing, pp. 24–51, doi:10.1007/978-3-319-23534-9_2, ISBN 978-3-319-23534-9, retrieved 2023-12-07
  7. Gurfinkel, Arie; Kahsai, Temesghen; Komuravelli, Anvesh; Navas, Jorge A. (2015). "The SeaHorn Verification Framework". In Kroening, Daniel; Păsăreanu, Corina S. (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 343–361. doi:10.1007/978-3-319-21690-4_20. ISBN 978-3-319-21690-4.
  8. Kahsai, Temesghen; Rümmer, Philipp; Sanchez, Huascar; Schäf, Martin (2016). "JayHorn: A Framework for Verifying Java programs". In Chaudhuri, Swarat; Farzan, Azadeh (eds.). Computer Aided Verification. Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 352–358. doi:10.1007/978-3-319-41528-4_19. ISBN 978-3-319-41528-4.
Category: