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.

• Type: Journal
• Year: 2011
• Where: APLAS
• Authors: Ashutosh Gupta, Corneliu Popeea, Andrey Rybalchenko
• Keywords: APLAS 2011, Functional Programs, Horn Clauses, Programming Languages, Uninterpreted Functions