Constrained Horn clauses explained

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

\phi\land P _{1(x} _{1)\land} \ldots\land P _{n( x _{n} )\to} P( x )

where

\phi is a constraint in some first-order theory, P _{i} are predicates, and x _{i} 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. The SeaHorn verifier for LLVM represents verification conditions as constrained Horn clauses,^[6] as does the JayHorn verifier for Java.^[7]

Notes and 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 . en . 22 . 6 . 974–1042 . 10.1017/S1471068421000211 . 236777105 . 1471-0684. CHCs are syntactically and semantically the same as constraint logic programs. free . 2108.00739 .
2. Cox . Jim . McAloon . Ken . Tretkoff . Carol . 1992-06-01 . Computational complexity and constraint logic programming languages . Annals of Mathematics and Artificial Intelligence . en . 5 . 2 . 163–189 . 10.1007/BF01543475 . 666608 . 1573-7470.
3. Book: Blicha . Martin . Britikov . Konstantin . Sharygina . Natasha . 2023 . Enea . Constantin . Lal . Akash . The Golem Horn Solver . https://link.springer.com/chapter/10.1007/978-3-031-37703-7_10 . Computer Aided Verification . Lecture Notes in Computer Science . en . Cham . Springer Nature Switzerland . 209–223 . 10.1007/978-3-031-37703-7_10 . 978-3-031-37703-7.
4. Book: Gurfinkel, Arie . 2022 . Shoham . Sharon . Vizel . Yakir . Program Verification with Constrained Horn Clauses (Invited Paper) . https://link.springer.com/chapter/10.1007/978-3-031-13185-1_2 . Computer Aided Verification . Lecture Notes in Computer Science . 13371 . en . Cham . Springer International Publishing . 19–29 . 10.1007/978-3-031-13185-1_2 . 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 . 10.4204/EPTCS.344.7 . 2109.04635v1 . 221132231 . en.
6. Book: Gurfinkel . Arie . Kahsai . Temesghen . Komuravelli . Anvesh . Navas . Jorge A. . 2015 . Kroening . Daniel . Păsăreanu . Corina S.. Corina Păsăreanu . The SeaHorn Verification Framework . https://link.springer.com/chapter/10.1007/978-3-319-21690-4_20 . Computer Aided Verification . Lecture Notes in Computer Science . en . Cham . Springer International Publishing . 343–361 . 10.1007/978-3-319-21690-4_20 . 978-3-319-21690-4.
7. Book: Kahsai . Temesghen . Rümmer . Philipp . Sanchez . Huascar . Schäf . Martin . 2016 . Chaudhuri . Swarat . Farzan . Azadeh . JayHorn: A Framework for Verifying Java programs . https://link.springer.com/chapter/10.1007/978-3-319-41528-4_19 . Computer Aided Verification . Lecture Notes in Computer Science . en . Cham . Springer International Publishing . 352–358 . 10.1007/978-3-319-41528-4_19 . 978-3-319-41528-4.