Constrained Horn clauses

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.^[1]

Definition

A constrained Horn clause is a formula of the form

${\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, ${\displaystyle P_{i}}$ are predicates, and ${\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.^[2]

Solvers

There are several automated solvers for CHCs,^[3] including the SPACER engine of Z3.^[4]

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

Applications

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

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.