TY - JOUR
T1 - Analysis and Transformation of Constrained Horn Clauses for Program Verification
AU - De Angelis, Emanuele
AU - Fioravanti, Fabio
AU - Gallagher, John Patrick
AU - Hermenegildo, Manuel V.
AU - Pettorossi, Alberto
AU - Proietti, Maurizio
PY - 2022
Y1 - 2022
N2 - This paper surveys recent work on applying analysis and transformation techniques that originate in the field of constraint logic programming (CLP) to the problem of verifying software systems. We present specialization-based techniques for translating verification problems for different programming languages, and in general software systems, into satisfiability problems for constrained Horn clauses (CHCs), a term that has become popular in the verification field to refer to CLP programs. Then, we describe static analysis techniques for CHCs that may be used for inferring relevant program properties, such as loop invariants. We also give an overview of some transformation techniques based on specialization and fold/unfold rules, which are useful for improving the effectiveness of CHC satisfiability tools. Finally, we discuss future developments in applying these techniques.
AB - This paper surveys recent work on applying analysis and transformation techniques that originate in the field of constraint logic programming (CLP) to the problem of verifying software systems. We present specialization-based techniques for translating verification problems for different programming languages, and in general software systems, into satisfiability problems for constrained Horn clauses (CHCs), a term that has become popular in the verification field to refer to CLP programs. Then, we describe static analysis techniques for CHCs that may be used for inferring relevant program properties, such as loop invariants. We also give an overview of some transformation techniques based on specialization and fold/unfold rules, which are useful for improving the effectiveness of CHC satisfiability tools. Finally, we discuss future developments in applying these techniques.
KW - Program verification
KW - Program analysis
KW - Program transformation
KW - Constrained horn clauses
KW - Comstraint logic programming
UR - https://arxiv.org/abs/2108.00739
U2 - 10.1017/S1471068421000211
DO - 10.1017/S1471068421000211
M3 - Journal article
VL - 22
SP - 974
EP - 1042
JO - Theory and Practice of Logic Programming
JF - Theory and Practice of Logic Programming
SN - 1471-0684
IS - 6
ER -