אירועים והרצאות בפקולטה למדעי המחשב ע"ש הנרי ומרילין טאוב

Constrained Horn Clauses (CHCs) is a fragment of First Order Logic (FOL), that has gained a lot of attention in recent years. One of the main reasons for the rising interest in CHCs is the ability to reduce many verification problems to satisfiability of CHCs. For example, program verification can naturally be described as the satisfiability of CHCs modulo a background theory such as linear arithmetic and arrays. To this end, CHC-solvers can be used as the back-end for different verification tools and allow to separate the generation of verification conditions from the decision procedure that decides if the verification conditions are correct or not. In our work, we present a novel framework, called LazyHorn, that is aimed at solving the satisfiability problem of CHCs modulo a background theory. The framework is driven by the idea that a set of CHCs can be solved in parts, making it an easier problem for the CHC-solver. Furthermore, solving a set of CHCs can benefit from an interpretation revealed by the solver for its subsets. LazyHorn is lazy in that it gradually extends the set of checked CHCs, as needed. It is also incremental in its use of a CHC solver, supplying it with an interpretation, obtained for previously checked subsets. We have implemented an efficient instance of the framework that is restricted to a fragment of CHCs called linear CHCs.