• Images
• Videos
• Documents
• Books
• Articles

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 https://doi.org/10.1017%2FS1471068421000211 ↩

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. https://doi.org/10.1007/BF01543475 ↩

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. 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. 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. /wiki/ArXiv_(identifier) ↩

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 978-3-319-23534-9 ↩

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. 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. 978-3-319-41528-4 ↩