Constrained Horn clauses
 | This article is missing information about if they are named after somebody? When were they first defined? Perhaps add an example?. (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.[1]
Definition
[edit]A constrained Horn clause is a formula of the form
where is a constraint in some first-order theory, are predicates, and are universally-quantified variables. The addition of constraint makes it a generalization of the plain Horn clause.
Decidability
[edit]The satisfiability of constrained Horn clauses with constraints from linear integer arithmetic is undecidable.[2]
Solvers
[edit]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
[edit]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
[edit]- ^ 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
- ^ 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.
- ^ 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.
- ^ 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.
- ^ 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.
- ^ 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
- ^ 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.
- ^ 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.