PVAIR: Partial Variable Assignment InterpolatoR
 3 Citations
 705 Downloads
Abstract
Despite its recent popularity, program verification has to face practical limitations hindering its everyday use. One of these issues is scalability, both in terms of time and memory consumption. In this paper, we present Partial Variable Assignment InterpolatoR (PVAIR) – an interpolation tool exploiting partial variable assignments to significantly improve performance when computing several specialized Craig interpolants from a single proof. Subsequent interpolant processing during the verification process can thus be more efficient, improving scalability of the verification as such. We show with a wide range of experiments how our methods improve the interpolant computation in terms of their size. In particular, (i) we used benchmarks from the SAT competition and (ii) performed experiments in the domain of software upgrade checking.
1 Introduction
Symbolic modelchecking algorithms rely on expressing a verification problem as a logical formula and determining whether the formula satisfies a given property. Many subtasks of modelchecking, such as computing safe inductive invariants for programs and summarizing functionality with respect to properties critical to program correctness, rely on overapproximating parts of the formula. To keep the formal verification manageable and the run time low it is critical that the overapproximations are suitable for the modelchecking task at hand. Craig interpolation [7] is a process for computing overapproximations of firstorder formulas that has proven useful in both program verification and automatic approximation refinement [15]. The idea in applying Craig interpolation in model checking is to reduce the overapproximation process into finding a compact interpolant I such that I is satisfied by all models of the part being overapproximated but still entails the properties of interest with respect to the rest of the formula. The Labeled Interpolation System (LIS) [8] is a widely used framework for computing Craig interpolants in propositional logic from a resolution refutation. The flexibility of LIS allows it to be used in a variety of verification tasks that place additional requirements for the interpolants [18].
In some tasks, (e.g., when proving safety of certain types of program updates or speeding up modelchecking with parallel computing) it is useful to compute overapproximations of the formula under assumptions which are specific to the particular application problem. However, the LIS framework in its original form does not allow for computing interpolants under assumptions. There are several reasons why such focused interpolants would be beneficial in particular in the LIS framework. Firstly, the focused interpolants are in general smaller and therefore more manageable for the model checker. Secondly, the properties of interpolants provided by the LIS framework, such as the path interpolation property [13], can be preserved in the focused interpolants. Thirdly, several focused interpolants can be computed from a single resolution refutation, while constructing a resolution refutation is computationally expensive. In [12], we introduced an interpolation system exploiting partial variable assignments to improve efficiency of interpolant computation. We proved that following a set of requirements put on labeling during interpolation results in interpolants with the path interpolation property, which is required by some verification tools, e.g. [1], to work.
This paper presents the Partial Variable Assignment InterpolatoR (PVAIR), the first implementation that is able to construct such focused interpolants. The implementation is based on the Labeled Partial Assignment Interpolation System (LPAIS) [12], an extension of LIS which supports focusing the interpolant in the manner required by the verification applications. The PVAIR solution is generic and can be used in various model checkingbased scenarios. In this paper, in addition to providing the description of the tool architecture, we also report an initial experimental study on how the interpolants constructed with PVAIR behave in different example tasks. The results show a significant improvement in both interpolant size and the overall model checking time, suggesting that the approach is viable for constructing focused interpolants.
The general intuition behind the applications of PVAIR is that sometimes a symbolic model checker can provide a partial truth assignment for the formula being verified, coming from the knowledge of the program structure and meaning of the variables. As a result, some constraints of the formula can get satisfied; the LPAIS framework allows for removing such clauses during the interpolant computation. This improves the interpolation in two ways: the interpolation becomes faster, and the resulting interpolant can be significantly smaller. Because of the latter the interpolants can be handled in a more efficient way during the subsequent computation. PVAIR is built on top of the opensource tool PeRIPLO [18], which provides resolution proofs and is able to optimize the proofs for interpolation through transformations. PeRIPLO has been used in various verification projects, including function summarization in eVolCheck [10] and FunFrog [22], both as an interpolation engine and as a SAT solver.
We experimentally studied the performance of PVAIR on a set of its potential applications. We compared it to PeRIPLO during computation of a summary for a particular function using eVolCheck . In this experiment, PVAIR was used to rule out the program paths that do not call the function. We also applied PVAIR in more generic settings, when constructing interpolation problems from a subset of the SAT Competition benchmarks. This experiment resembles closely the scenario of computing focused interpolants for a divideandconquer approach for parallel model checking. In both types of benchmarks, we report a substantial reduction in interpolant sizes. As shown in the eVolCheck use case, smaller interpolants also result in considerably faster upgradechecking steps.
2 Preliminaries and Background Theory
A literal is a Boolean variable l or its negation \(\bar{l}\). A clause is a disjunction over a set of literals. We use angle brackets \(\langle \varTheta \rangle \) to denote the clause built from the literals in set \(\varTheta \). A propositional formula in Conjunctive Normal Form (CNF) is a conjunction (or equivalently set) of clauses. A resolution proof for a set of clauses \(\varPhi \) is a rooted DAG with each node having either no antecedents (leaf node) or exactly two antecedents (inner node). Each node in the resolution proof is associated with node clause; from now on we use proof node and corresponding node clause equivalently. A leaf node corresponds to an input clause from \(\varPhi \). Each inner node with two antecedents \(\langle \varTheta _1, p \rangle \) and \(\langle \varTheta _2, \bar{p} \rangle \) has node clause \(\langle \varTheta _1, \varTheta _2 \rangle \), thus representing a resolution where p is the pivot variable.
Given an unsatisfiable CNF formula \(\varPhi \) and its (A,B)partitioning into \(A \wedge B\) parts, a Craig interpolant [7] is a formula I such that I is implied by A (\(\models A \mathop {\Rightarrow }\limits ^{} I\)), unsatisfiable with B (\(\models B \wedge I \mathop {\Rightarrow }\limits ^{} \bot {}\)), and defined over common symbols (variables) of A and B. An interpolant can be seen as an overapproximation of A still being strong enough to be unsatisfiable with B.
As an overapproximation, Craig interpolants express properties for all models of the formula. However, this might be unnecessarily strong for some applications. For example, while constructing a function summary through interpolation, it is possible to consider only the models corresponding to the paths going via the summarized function. Based on the encoding of the function body, a variable assignment blocking all the other paths can be derived. This applies also for the case of Abstract Reachability Graphs (ARGs). The label of a particular ARG node is an overapproximation of reachable states at that node. Since the paths in ARG which do not go via the node cannot influence the reachable states at that node, for each node it is possible to compute variable assignment blocking these paths; in other words, the assignment permits only the models corresponding to paths via the node. The node labels are computed by interpolation, however it is actually enough to compute a formula that is an interpolant for the models consistent with the assignment.
Focused Interpolants. A Partial Variable Assignment (PVA ) \(\pi \) assigns value True resp. False to some variables from formula \(\varPhi \); alternatively, PVA can be seen as a conjunction of literals. Given a partial variable assignment \(\pi \), a set of clauses A can be partitioned into \(A_{\pi }\) – a subset of clauses from A satisfied by the assignment, and the remaining clauses \(A_{\overline{\pi }}\) which are not satisfied by \(\pi \). For a given unsatisfiable formula \(\varPhi \), its partitioning into \(A \wedge B\) and a partial variable assignment \(\pi \), a Partial Variable Assignment Interpolant [12], shortly focused interpolant, is a formula I such that \(\pi \models A \mathop {\Rightarrow }\limits ^{} I\) and \(\pi \models B \wedge I \mathop {\Rightarrow }\limits ^{} \bot {}\) and I is defined over unassigned shared variables between \(A_{\overline{\pi }}\) and \(B_{\overline{\pi }}\), i.e., the symbols common to the \(\pi \)unsatisfied parts of A and B. In other words, it is an interpolant, but only for models which agree on the values of variables assigned by \(\pi \). Due to the weakened requirements, the focused interpolants can be of a smaller size compared to the Craig interpolants. The focused interpolants can be alternatively seen as Craig interpolants for the unsatisfied parts of the input – subproblem, i.e., for \(A_{\overline{\pi }} \wedge B_{\overline{\pi }}\) where literals falsified by the assignment are removed.
Example 1 (cont.): Let us assume assignment \(\pi \equiv \bar{l}_2\) (i.e., assigning False to variable \(l_2\)) and the set of clauses from our previous example. Given the assignment, B can be split into \(B_{\pi } \equiv \langle \bar{l}_2~\vee ~\bar{l}_6 \rangle \wedge \langle \bar{l}_2~\vee ~l_4 \rangle \) and \(B_{\overline{\pi }} \equiv \langle \bar{l}_4~\vee ~\bar{l}_5 \rangle \wedge \langle \bar{l}_1~\vee ~l_2 \rangle \). \(A_{\pi }\) is empty thus \(A_{\pi } \equiv \top {}\) and \(A_{\overline{\pi }} \equiv A\).
Craig and focused interpolants differ in the variables which could occur in the interpolant. The shared variables between A and B (i.e., those that can appear in a Craig interpolant) are \(l_1\), \(l_2\), \(l_5\) and \(l_6\). Since focused interpolants consider for the shared variables only unsatisfied parts of A resp. B (i.e., \(A_{\overline{\pi }}\) and \(B_{\overline{\pi }}\)), fewer variables are shared; in our example only \(l_1\) and \(l_5\) could appear in a focused interpolant, which are those which can appear in a Craig interpolant for the subproblem.
Labeled Partial Assignment Interpolation System
Labeled Partial Assignment Interpolation System (LPAIS ) — an extension of the Labeled Interpolation System [8] — yields focused interpolants from the resolution refutation of \(A \wedge B\).
In LPAIS , each literal in the clauses of the resolution proof is assigned a label a, b, ab, or \(d^{+}\). Labels a, b, and ab have the same meaning as in LIS, while the label \(d^{+}\) is used for the literals from the assignment \(\pi \). The lattice of labels is defined by the Hasse diagram in Fig. 3. The labels are specified via a labeling function\(\mathsf {Lab}_{}\); e.g., \(\mathsf {Lab}_{}(v_2, \overline{p})\) is the label of literal \(\overline{p}\) at node \(v_2\) of the proof. The label of a literal in an inner node v is computed using join operator \(\sqcup \) (defined by Fig. 3) from the labels of the literal in the antecedent nodes (\(\mathsf {Lab}_{}(v, l) = \mathsf {Lab}_{}(v_1, l) \sqcup \mathsf {Lab}_{}(v_2, l)\), where \(v_1\) and \(v_2\) are the antecedent nodes of v). Formal definition of labeling function as well as the requirements that labels must satisfy are described in [12].
The labeled partial assignment interpolation system assigns a partial interpolant [I] to each proof node according to the rules described in Table 1. The partial interpolants of the leaf nodes are directly constructed from the node clauses (it means those forming \(A \wedge B\)) using the rules in the upper part of Table 1. The applied Hyp\(*\) rule is determined by the set inclusion check in the middle column; in particular by occurrence of the node clause in \(A_{\overline{\pi }}\), \(A_{\pi }\), \(B_{\pi }\) and \(B_{\overline{\pi }}\). A partial interpolant for the Hyp\(A_{\overline{\pi }}\) rule, defined as \(\langle \varTheta \rangle \!_{b, \pi }\), represents a clause which is created from the node clause \(\langle \varTheta \rangle \) by omitting the literals over the \(\pi \)assigned variables and those whose label differs from b. In particular node clause Open image in new window yields partial interpolant Open image in new window . The leaf nodes with clauses satisfied by \(\pi \) have the partial interpolant \(\top \).
For inner nodes, the rule from Table 1 is chosen based on the labels of the pivot in the antecedents (denoted by \(v_1\) and \(v_2\)). Note the Res\(d^{+}\) rules, which correspond to the case where the pivot is satisfied by the assignment in one of the antecedents. In these cases, the partial interpolant is the same as the partial interpolant in the antecedent not being satisfied by the assignment; due to such nodes the size of the LPAIS interpolant is smaller compared to the LIS interpolant.
Example 1 (cont.): Figure 5 shows how focused interpolant \(I_\pi \equiv l_1 \vee \bar{l}_3\) for our example can be derived. Note the dotted arrows at nodes corresponding to Res\(d^{+}\) resolutions; they highlight the antecedents whose partial interpolants are ignored and their subtrees do not contribute to final focused interpolant. Also note that the focused interpolant \(I_\pi \) is smaller compared to both \(I_1[\pi ]\) and \(I_2[\pi ]\) from the examples above.
An assignment applied onto (interpolant) formula (i.e., if \(I[\pi ]\) is computed) can reduce the size of the formula only if the assigned variable appears in the (interpolant) formula (i.e., the variable has to be shared). However, LPAIS reduce the size of the interpolants even if the assigned variable does not appear in the interpolant, since the reduction is done as a part of interpolant computation and not as a postprocessing step.
PVAIR implements the LPAIS framework. The tool can generate the McMillan’s [16], Pudlák’s [17], and McMillan’s\('\) [8] interpolants and their equivalents in presence of assignments. Additionally, PVAIR supports constructing different interpolants by providing different labelings for the literals in the leaves. The relative logical strength of interpolants constructed with LPAIS from the same resolution refutation is determined by the labeling function used. For instance, the McMillan’s focused interpolants are sufficiently strong to have the pathinterpolation property.
3 The Tool Architecture
The PVAIR architecture is shown in Fig. 6. It takes a propositional formula, its (A, B)partitioning, and a partial variable assignment as input and produces focused interpolants if the input formula is unsatisfiable. The input can be provided either in a file in the SMTLIB 2.0 format or via a C++ API.
The workflow of the PVAIR tool is as follows. First, the input formula is passed to the PeRIPLObased preprocessing module. Since the formula can be in an arbitrary form, it is transformed into CNF (the top box in Fig. 6) using an efficient, structuresharing version of the Tseitin encoding [25]. Its satisfiability is then determined using the MiniSAT 2.2.0 solver [9].
In the case of an unsatisfiable input, an initial refutation is extracted from the solver in the compact MiniSAT internal proof format. The format is then transformed into a resolution DAG to allow more efficient handling of the proof (Proof Construction). In particular, using the resolution DAG form, the proof can be compressed using wellknown proof reduction techniques such as structural hashing or pivot recycling [19, 20] available in PeRIPLO (Proof Reduction). The proof reduction techniques can be enabled/disabled via a configuration file or API.
Once the resolution proof R is computed, it is passed together with the partitionings and variable assignments to the interpolation engine (the bottom box in Fig. 6). From this point on, any number of partial variable assignments \(\pi _i\) and partitionings \(P_i\) (into \(A_i \wedge B_i\)) can be given as input to the tool and used to construct the corresponding interpolants \(I_i\). Note that in any case only one SATsolver call will be made during the entire execution. The first step inside the PVA interpolation engine is labeling all the literals in \(A \wedge B\). The \(d^{+}\)Labeler will distribute \(d^{+}\) labels among the literals according to the assigned variables, whereas the LIS will label the remaining literals according to the partitioning and the selected LISbased interpolation algorithm (which can be chosen in the configuration file or via API). When the labeling is complete, it is used together with the partitioning and resolution proof R to compute interpolants (Interpolant Construction).
The construction starts by computing partial interpolants (according to the upper part of Table 1) for the leaf nodes of the refutation. The computation then proceeds from the leaves to the root node. In each inner node, depending on the label of the pivot, a partial interpolant of the node is computed by combining the partial interpolants from the antecedent nodes (the bottom part of Table 1). During the interpolant construction partial interpolants are optimized using Boolean constant propagation and structural sharing (hashing). The final interpolant is computed in the root node.
4 Experiments
We ran PVAIR on two types of experiments: (1) SAT Competition benchmarks and (2) computational problems generated by the eVolCheck tool during verification procedure. To demonstrate the tool performance, we measured the size of produced interpolants and its effect on the total verification time.
4.1 SAT Competition
From the way focused interpolants are computed by PVAIR it is obvious that they are smaller compared to the Craig interpolants. In this part we illustrate the actual difference. Compared to experiments on functions summaries in the latter part, SAT Competition provides us with a larger set of more heterogeneous kinds of benchmarks. This helps one to see how the reduction of the size varies among inputs from different domains.
For experiments, we chose 47 unsatisfiable benchmarks from the SAT Competition^{1} from all categories – 12 from the Application (APP), 11 from the Crafted (CRF), and 24 from the Random (RND) sets. Since the benchmarks are not partitioned, we generated six partitionings for each benchmark; we simulated the typical way the path interpolants are computed, i.e., we randomly chose n, first n clauses of the benchmark belonged to the Apart, the remaining clauses to the Bpart. No assignment is given by authors of the benchmarks, thus for each partitioning we generated five random variable assignments consisting of a single, five, resp. twenty assigned variables. Assignments of various sizes indicate how the reduction scales w.r.t. the number of assigned variables.
Since focused interpolants can be seen as Craig interpolants for a subproblem, for each pair of partitioning and assignment, we created the subproblem instance and used PVAIR to computed the Craig interpolant. Subproblems are simpler compared to the benchmark from which they were generated, so interpolants for subproblems are typically smaller compared to Craig interpolants of the benchmark. However, the interpolant for each subproblem is computed from a different refutation proof; in contrast to focused interpolants which, for a particular benchmark, are all computed from the same proof. The path interpolation property [13], which is often exploited during program model checking, might be missing in this case.
As to the interpretation of the results: No assignment reflects the stateoftheart approaches, where Craig interpolants are used directly. Focused interpolants show how the size of the interpolants can be reduced if the model checker (i.e., a tool generation the input) provides a reasonable assignment together with a partitioning. The interpolants for a subproblem can be seen as an alternative to focused interpolants because of their similar meaning, however these interpolants lack the properties of the focused ones.
Average interpolant sizes by category and number of assigned variables.
Figure 7 compares the sizes of the computed interpolants. Each point in the graph corresponds to a single partitioning of a benchmark; the xaxis represents the interpolant size if no assignment is provided (Craig interpolant) while the yaxis represents the size of the focused interpolants with a single (resp. five) assigned variable(s). For presentation clarity, the yaxis is the average size of all five random assignments generated for a given partitioning. The values on axes represent millions of nodes if an interpolant is represented as DAG (counting literals and Boolean operators). The orange dashed line shows the average size of Craig interpolants for subproblems. This illustrates what price is paid by focused interpolants for the path interpolation property and a single SAT solver call. Both graphs show interesting reduction in size for focused interpolants as well as substantially larger reduction in case of five assigned variables. In both graphs the same partition of the same benchmark share the same xvalue, thus it is possible, especially for the larger ones, to compare their reductions.
Table 2 summarizes the results shown in the graphs above, reporting precise numbers. The table on the lefthand side compares the sizes of focused interpolants to Craig interpolants (in the No assignment row). The No assignment row shows the average size of Craig interpolants for a given benchmark type. The remaining rows show the relative sizes of focused interpolants w.r.t. the No assignment row. The application benchmarks exhibit a smaller reduction compared to the other types, and even for twenty assigned variables, the interpolants are half in the size of the Craig interpolants. The table on the righthand side compares the sizes of Craig interpolants for the benchmark with the Craig interpolants for subproblems (corresponding to the assignments used in the left table). The table shows that these interpolants are on average smaller compared to the focused ones. The more variables are assigned, the bigger the difference is. While the sizes are comparable for a few assigned variables, the price paid for the path interpolation property of focused interpolants is high for larger assignments (e.g., twenty variables).
Time and memory demands are crucial properties of each interpolation tool. The reduction in overall running time and required memory roughly correspond to the reduction of interpolant sizes; e.g., PVAIR is 11 % faster and requires 9 % less memory on average if a single variable is assigned. The time and memory savings occur as well during the interpolant computation phase due to smaller interpolants being handled.
4.2 Applying PVAIR for Checking Software Upgrades
The usefulness of PVAIR is motivated by the tremendous role of interpolation in model checking. One of the possible applications of PVAIR is checking software upgrades by means of function summarization [23] implemented in the tool eVolCheck. Given a program S and an assertion a, eVolCheck verifies S with respect to a (i.e., proves that \(S \wedge \lnot {a}\) is unsatisfiable) and, for each function call in S, it constructs the interpolant and treats it as a function summary. In [21] we show that even if the constructed function summary is an overapproximation of the function behavior of S, it preserves the safety of the assertion a in S.
eVolCheckvalidates the computed function summaries to overapproximate the behavior of the corresponding functions of a program upgrade, U. In that context, programs S and U must have a nonempty set of common function calls. eVolCheck traverses this set starting from the deepest level of the (unwound during preprocessing) function calltree and checks whether each original function summary still overapproximates the new behavior of the corresponding function. If there is a function call, the original summary of which does not overapproximate the new behavior, eVolCheck propagates the check to the caller function. If there is no function to propagate then U is unsafe. If at some depth of the unwound calltree all the function summaries are proven to be valid, then U is safe, and eVolCheck reconstructs the summaries for the modified function calls.
Applying PVAIR to eVolCheck. Consider the case when U is obtained from S by removing some functionality. Then by construction, the original summaries of S are still valid overapproximation of the new function behavior in U. But at the same time, they might be unnecessarily general and consume excessive memory. While the use of the original summaries does not break soundness of the further upgrade checking, it is practical to refresh (and possibly shrink) the summaries to become more accurate with respect to U.
The refreshed summaries may be used to verify a further updated program W that additionally may introduce new functionality with respect to U. On the other hand, the summaries may be also used to speed up verification of a new assertion b, implanted in the code of U [21]. To enable both scenarios, the constructed summaries need to be externally stored and further migrated across the verification runs. Thus, the size of the summary also becomes important.
While eVolCheck does not provide a way to refresh summaries except of complete reverification of U from scratch, PVAIR becomes particularly useful. Let \(\varDelta _{S,U}\) denote the behavioral difference of S and U, i.e., the set of behaviors of S not present in U. If the set \(\varDelta _{S,U}\) is nonempty, it could be exploited by PVAIR to generate the partial interpolants that represent new summaries for each function in U. These updated summaries are still guaranteed to preserve safety of the assertion a in U.
Experiments. We experimented with PVAIR on a set of 10 pairs of different benchmarks written in C. Notably, all benchmarks used nonlinear arithmetic operations. After the required propositional encoding (i.e., bitblasting), the resulting largesize formulae have been a bottleneck for solving and interpolation using the original eVolCheck approach.
In our experiments, for each pair of programs, S and U, we obtained U from the corresponding S by assigning guards in some conditional expressions. In particular, we replaced if P do A else do B by assume(P); A. This is equivalent to assigning P = true, and \(\varDelta _{S,U}\) consists of the behaviors specified by assume(\(\lnot \)P); B. For simplicity, in our experiments, we assumed that \(\varDelta _{S,U}\) affected only a single function f.

the use of PVAIR yields smaller summaries compared to the ones by PeRIPLO,

the use of smaller summaries improves the overall performance of eVolCheck.
We collected the size of the resulting interpolants and total verification time needed to perform steps (1) and (2). We used the Pudlák interpolation algorithm [17] to construct the “orig” interpolants (the ones constructed without \(\varDelta _{S,U}\)).
eVolCheck verification statistics.
C program  Interpolant (function summary) size  Verification time (sec)  

name  # var. assigned  # var. orig.  # var. PVAI  # cl. orig  # cl. PVAI  boot. orig.  boot. PVAI  upgr. orig.  upgr. PVAI 
Test 0  3 vars  15227  62.61 %  45192  62.21 %  18.93  99.17 %  4.025  65.96 % 
Test 1  1 var  23273  78.46 %  69330  78.31 %  10.36  99.24 %  4.034  77.79 % 
Test 2  2 vars  31278  59.19 %  93345  58.98 %  8.71  100.32 %  3.878  57.61 % 
Test 3  1 var  12236  63.80 %  36219  63.31 %  7.34  100.12 %  1.256  71.50 % 
Test 4  2 vars  20447  74.57 %  60852  74.37 %  12.40  101.94 %  2.982  81.35 % 
Test 5  3 vars  24716  32.50 %  73659  32.05 %  12.20  102.94 %  3.855  39.46 % 
Test 6  3 vars  33076  37.89 %  98739  37.58 %  12.63  102.16 %  7.951  40.05 % 
Test 7  1 var  12478  57.47 %  36945  56.91 %  8.88  100.29 %  2.350  57.96 % 
Test 8  1 var  21201  50.42 %  63114  50.04 %  14.46  97.55 %  3.706  50.94 % 
Test 9  2 vars  20314  39.71 %  60453  39.22 %  21.42  101.26 %  4.581  40.30 % 
5 Related Work
This section compares the PVAIR approach with various techniques for reducing the size of an interpolant based on variable assignments, proof compression, and interpolant postprocessing.
Variable Assignments. Given a variable assignment, the most straightforward way to reduce the interpolant size is to apply the assignment directly onto the interpolant formula and propagate Boolean constants. This idea is used in the UFO [1] tool. Due to the tight integration into the interpolation process, LPAIS yields smaller interpolants compared to this simple approach. Since the assignment is considered by LPAIS already during the interpolant construction, this results in larger parts of the interpolant being cut away.
Proof Compression. Interpolants are often derived from a resolution proof and therefore their size is roughly proportional to the size of the proof. Several methods for compressing a resolution proof exist [2, 4, 6, 11, 19]. Different variants of these techniques are applied in PdTRAV [5] verification framework, the PeRIPLO tool, and the Skeptik [3] proof transformer, just to name a few examples. In this work, the reduction of the interpolant size is based on the fact that only a proof of the unsatisfied part of the input formula is needed. Since the omitted (i.e., satisfied) parts can be important w.r.t. other assignments, the proof compression techniques cannot remove these parts from the proof. As a result, these techniques are orthogonal and PVAIR can benefit from proof compression if applied.
Interpolant Postprocessing. Once an interpolant is computed, various techniques can be used to reduce its size. Such techniques include constant propagation, structural sharing, and various equivalence and subsumption checks. PdTRAV, for example, internally uses BDDbased sweeping to detect the equivalences and balancing/rewriting over AndInverter Graphs [14] representation to further reduce the size of an interpolant. Any such postprocessing technique producing smaller equivalent formulae can be applied to the interpolants produced by the PVAIR tool.
6 Conclusions
In this paper we presented the PVAIR interpolation tool, which exploits partial variable assignments obtained from an applicationspecific source to compute focused interpolants. The tool uses the extension of the labeled interpolation system, LPAIS, to construct the interpolants from a resolution refutation. We presented a potential application for the focused interpolants, in particular in software upgrade checking where we require the path interpolation property. We performed an initial study using a wide range of experiments varying the size of the partial variable assignment. The results show a good improvement compared to the baseline and suggest that the approach taken for computing focused interpolants has significant potential in reducing the interpolant size and model checking time. In the future we plan to integrate the PVAIR tool into a concrete implementation of a parallel model checker as well as to study other applications of model checking where partial assignments arise naturally.
Footnotes
References
 1.Albarghouthi, A., Gurfinkel, A., Chechik, M.: From underapproximations to overapproximations and back. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 157–172. Springer, Heidelberg (2012)CrossRefGoogle Scholar
 2.BarIlan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Lineartime reductions of resolution proofs. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 114–128. Springer, Heidelberg (2009)CrossRefGoogle Scholar
 3.Boudou, J., Fellner, A., Woltzenlogel Paleo, B.: Skeptik: a proof compression system. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 374–380. Springer, Heidelberg (2014)Google Scholar
 4.Boudou, J., Woltzenlogel Paleo, B.: Compression of propositional resolution proofs by lowering subproofs. In: Galmiche, D., LarcheyWendling, D. (eds.) TABLEAUX 2013. LNCS, vol. 8123, pp. 59–73. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 5.Cabodi, G., Loiacono, C., Vendraminetto, D.: Optimization techniques for craig interpolant compaction in unbounded model checking. In: DATE, pp. 1417–1422 (2013)Google Scholar
 6.Cotton, S.: Two techniques for minimizing resolution proofs. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 306–312. Springer, Heidelberg (2010)CrossRefGoogle Scholar
 7.Craig, W.: Three uses of the HerbrandGentzen theorem in relating model theory and proof theory. Symbol. Logic 22, 269–285 (1957)MathSciNetCrossRefzbMATHGoogle Scholar
 8.D’Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 129–145. Springer, Heidelberg (2010)CrossRefGoogle Scholar
 9.Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005)CrossRefGoogle Scholar
 10.Fedyukovich, G., Sery, O., Sharygina, N.: eVolCheck: incremental upgrade checker for C. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 292–307. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 11.Fontaine, P., Merz, S., Woltzenlogel Paleo, B.: Compression of propositional resolution proofs via partial regularization. In: Bjørner, N., SofronieStokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 237–251. Springer, Heidelberg (2011)CrossRefGoogle Scholar
 12.Jancik, P., Kofroň, J., Rollini, S.F., Sharygina, N.: On interpolants and variable assignments. In: FMCAD, pp. 123–130 (2014)Google Scholar
 13.Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 459–473. Springer, Heidelberg (2006)CrossRefGoogle Scholar
 14.Kuehlmann, A., Ganai, M.K., Paruthi, V.: Circuitbased Boolean reasoning. In: DAC, pp. 232–237 (2001)Google Scholar
 15.McMillan, K.L.: Interpolation and SATbased model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)CrossRefGoogle Scholar
 16.McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16–30. Springer, Heidelberg (2004)CrossRefGoogle Scholar
 17.Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. Symbol. Logic 62, 981–998 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
 18.Rollini, S.F., Alt, L., Fedyukovich, G., Hyvärinen, A.E.J., Sharygina, N.: PeRIPLO: a framework for producing effective interpolants in SATbased software verification. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR19 2013. LNCS, vol. 8312, pp. 683–693. Springer, Heidelberg (2013)CrossRefGoogle Scholar
 19.Rollini, S.F., Bruttomesso, R., Sharygina, N., Tsitovich, A.: Resolution proof transformation for compression and interpolation. Formal Methods Syst. Des. 45, 1–41 (2014)CrossRefzbMATHGoogle Scholar
 20.Rollini, S.F., Sery, O., Sharygina, N.: Leveraging interpolant strength in model checking. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 193–209. Springer, Heidelberg (2012)CrossRefGoogle Scholar
 21.Sery, O., Fedyukovich, G., Sharygina, N.: Interpolationbased function summaries in bounded model checking. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 160–175. Springer, Heidelberg (2012)CrossRefGoogle Scholar
 22.Sery, O., Fedyukovich, G., Sharygina, N.: FunFrog: bounded model checking with interpolationbased function summarization. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 203–207. Springer, Heidelberg (2012)CrossRefGoogle Scholar
 23.Sery, O., Fedyukovich, G., Sharygina, N.: Incremental upgrade checking by means of interpolationbased function summaries. In: FMCAD, pp. 114–121 (2012)Google Scholar
 24.Tange, O.: GNU parallel  the commandline power tool. In: The USENIX Magazine, pp. 42–47 (2011)Google Scholar
 25.Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, pp. 115–125. Plenum, New York (1969)Google Scholar