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
where is a constraint in some first-order theory, are predicates, and are universally-quantified variables.
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
- ^ 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). Enea, Constantin; Lal, Akash (eds.). The Golem Horn Solver. 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.
{{cite book}}:|journal=ignored (help) - ^ Gurfinkel, Arie (2022). Shoham, Sharon; Vizel, Yakir (eds.). Program Verification with Constrained Horn Clauses (Invited Paper). 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.
{{cite book}}:|journal=ignored (help) - ^ 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). Kroening, Daniel; Păsăreanu, Corina S. (eds.). The SeaHorn Verification Framework. 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.
{{cite book}}:|journal=ignored (help) - ^ Kahsai, Temesghen; Rümmer, Philipp; Sanchez, Huascar; Schäf, Martin (2016). Chaudhuri, Swarat; Farzan, Azadeh (eds.). JayHorn: A Framework for Verifying Java programs. 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.
{{cite book}}:|journal=ignored (help)
This page was last edited on 25 January 2024, at 20:56