On Solving Universally Quantified Horn Clauses

Program proving can be viewed as solving for unknown relations (such

as loop invariants, procedure summaries and so on) that occur in the

logical verification conditions of a program, such that the

verification conditions are valid. Generic logical tools exist that

can solve such problems modulo certain background theories, and

therefore can be used for program analysis. Here, we extend these

techniques to solve for quantified relations. This makes it

possible to guide the solver by constraining the form of the proof,

allowing it to converge when it otherwise would not. We show how to

simulate existing abstract domains in this way, without having to directly

implement program analyses or make certain heuristic choices, such as

the terms and predicates that form the parameters of the abstract

domain. Moreover, the approach gives the flexibility to go beyond

these domains and experiment quickly with various invariant forms.

In  Static Analysis Symposium

Publisher  Springer


> Publications > On Solving Universally Quantified Horn Clauses