Appeared at DAC’03A Hybrid SAT-Based Decision Procedure for SeparationLogic with Uninterpreted Functions∗Sanjit A. [email protected] K. [email protected] E. [email protected] of Computer Science & Department of Electrical and Computer EngineeringCarnegie Mellon University, Pittsburgh, PA 15213ABSTRACTSAT-based decision procedures for quantifier-free fragments of first-order logic have proved to be useful in formal verification. Thesedecision procedures are either based on encoding atomic subfor-mulas with Boolean variables, or by encoding integer variables asbit-vectors. Based on evaluating these two encoding methods ona diverse set of hardware and software benchmarks, we concludethat neither method is robust to variations in formula characteris-tics. We therefore propose a new hybrid technique that combinesthe two methods. We give experimental results showing that the hy-brid method can significantly outperform either approach as well asother decision procedures.Categories and Subject DescriptorsI.1 [Symbolic and Algebraic Manipulation]: Expressions andTheir Representation, Algorithms; I.2.3 [Deduction and TheoremProving]; F.4.1 [Mathematical Logic]: Mechanical theorem prov-ingGeneral TermsAlgorithms, Experimentation, Measurement, VerificationKeywordsDesign verification, Decision procedures, Boolean satisfiability, The-orem proving.1. INTRODUCTIONQuantifier-free fragments of first-order logic and decision proce-dures for them have become commonplace in many formal verifi-cation efforts. Decision procedures for the Logic of Equality withUninterpreted Functions(EUF) have been successfully used in theautomated verification of pipelined processor designs [8, 4]. Pred-icate abstraction methods [9] based on decision procedures have∗This work was supported by ARO grant DAAD19-01-1-0485 andSRC contract 1029.001.Permission to make digital or hard copies of all or part of this work forpersonal or classroom use is granted without fee provided that copies arenot made or distributed for profit or commercial advantage and that copiesbear this notice and the full citation on the first page. To copy otherwise, torepublish, to post on servers or to redistribute to lists, requires prior specificpermission and/or a fee.DAC 2003, June 2–6, 2003, Anaheim, California, USA.Copyright 2003 ACM 1-58113-688-9/03/0001 ...$5.00.been used to verify parameterized cache coherence protocols. Thelogic of Counter Arithmetic with Lambda Expressions and Unin-terpreted Functions [6] (CLU), which generalizes EUF, is the basisfor the UCLID verifier which has been used for bounded modelchecking and inductive invariant checking of out-of-order micro-processors with unbounded resources [11]. Decision proceduresare an integral part of software verification systems including theCode Validation tool [13] and the Blast verifier [10]. Hence theimportance of having efficient decision procedures can hardly beoverstated.Many decision procedures leverage off the recent advances in Booleansatisfiability (SAT) solvers. These decision procedures differ in theBoolean encoding and the degree of the coupling with the SATsolver. One can classify these procedures as being either eageror lazy. In the eager approaches [4, 6, 12, 14], the quantifier-free first-order formula is converted in a single step to an equiva-lent Boolean formula which is checked using the SAT solver. Thelazy approaches (e.g., [3, 1]) iteratively refine the Boolean encod-ing based on satisfying assignments from the SAT solver that areinconsistent with the first order theory. The process is repeated untila consistent assignment is found or all assignments are explored.We consider the problem of deciding formulas in the logic of Sep-aration Predicates and Uninterpreted Functions (SUF), which canexpress properties of systems modeled in CLU logic. For deci-sion procedures using the eager approach, two Boolean encodingmethods have been proposed: small-domain encoding (also calledfinite instantiation) [6], and per-constraint encoding [14]. In small-domain encoding, each integer variable is interpreted over a finiteset of values that is determined by analyzing the formula. On theother hand, in per-constraint encoding, each atomic subformula isencoded as a Boolean variable. Constraints are then added to pruneoff the inconsistent assignments of the Boolean variables.In this paper, we confirm results of our previous experimental eval-uation [5] of these two encoding methods, concluding that neitherof the approaches are robust to variations in formula characteris-tics. Hence, we propose a new hybrid method that combines thetwo methods, and show that it can be more robust than either ap-proach. Finally, we report empirical results comparing our hybridmethod with other decision procedures for SUF logic.2. BACKGROUNDFigure 1 summarizes the expression syntax for SUF logic. Expres-sions can be of two types: integer or Boolean. Boolean expressionsare formed by combining equalities, inequalities, or applicationsof uninterpreted predicates using Boolean connectives. Integer ex-pressions are formed by applying an uninterpreted function to a listof integer expressions, by applying the unary arithmetic functionssucc (“+1”) and pred (“−1”), or by applying the ITE (“if-then-else”) operator. We will omit parentheses for function and pred-bool-expr ::= true | false |¬bool-expr | (bool-expr ∧bool-expr)| (int-expr=int-expr) |(int-expr < int-expr)| predicate-symbol(int-expr, . . . , int-expr)int-expr ::= ITE(bool-expr, int-expr, int-expr)| succ(int-expr) |pred(int-expr)| function-symbol(int-expr, . . . , int-expr)Figure 1: SUF Syntax.icate symbols with zero arguments, writing a instead of a(). Werefer to function symbols of zero arity as symbolic constants, andto predicate symbols of zero arity as symbolic Boolean constants.Uninterpreted functions and predicates are used in hardware de-sign verification to abstract word-level values of data and imple-mentation details of functional blocks. These functions and pred-icates satisfy no particular property other than functional consis-tency, viz., that they evaluate to the same value on the same argu-ments. Adding equalities, inequalities, and interpreted functionssucc and pred facilitates reasoning about ordering and equality ofdata values, and modeling ordered data structures such as queues.2.1 Decision Procedure OverviewAssume we start with a well-formed formula