Solving Recursion-Free Horn Clauses over LI+UIF

10 years 5 months ago
Solving Recursion-Free Horn Clauses over LI+UIF
Verification of programs with procedures, multi-threaded programs, and higher-order functional programs can be effectively auusing abstraction and refinement schemes that rely on spurious counterexamples for abstraction discovery. The analysis of counterexamples can be automated by a series of interpolation queries, or, alternatively, 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 resolution to deal with the clausal structure and relies on partial solutions to deal with (non-local) instances of functionality axioms.
Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenk
Added 12 Dec 2011
Updated 12 Dec 2011
Type Journal
Year 2011
Authors Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko
Comments (0)