@inproceedings{3264, abstract = {Verification of programs with procedures, multi-threaded programs, and higher-order functional programs can be effectively au- tomated using abstraction and refinement schemes that rely on spurious counterexamples for abstraction discovery. The analysis of counterexam- ples can be automated by a series of interpolation queries, or, alterna- tively, as a constraint solving query expressed by a set of recursion free Horn clauses. (A set of interpolation queries can be formulated as a single constraint over Horn clauses with linear dependency structure between the unknown relations.) In this paper we present an algorithm for solving recursion free Horn clauses over a combined theory of linear real/rational arithmetic and uninterpreted functions. Our algorithm performs resolu- tion to deal with the clausal structure and relies on partial solutions to deal with (non-local) instances of functionality axioms.}, author = {Gupta, Ashutosh and Popeea, Corneliu and Rybalchenko, Andrey}, editor = {Yang, Hongseok}, location = {Kenting, Taiwan}, pages = {188 -- 203}, publisher = {Springer}, title = {{Solving recursion-free Horn clauses over LI+UIF}}, doi = {10.1007/978-3-642-25318-8_16}, volume = {7078}, year = {2011}, }