IPRA 2014 PROCEEDINGS: PAPERS WITH ABSTRACTS

This talk is a tutorial on interpolation in verification.

Model checking is an automatic approach to formally verify that a given system satisfies a given specification. SAT-based model checking is most efficient in finding bugs in large systems. When combined with interpolation, it can also provide full verification.

We describe the use of interpolation in SAT-based model checking and survey several approaches to enhance its power.

We will assume no previous knowledge on model checking or interpolation. All the needed background will be given.

We discuss the role of (variants of) Craig interpolation in description logic research. We start by considering Craig interpolation itself and how it is related to the structure of ontologies and the rewritability of queries in ontology-based data access. We then briefly discuss the role of parallel interpolation (introduced more recently by Parikh et al) for decomposing ontologies. Finally, we consider uniform interpolation - an extension of Craig interpolation in which the interpolant is independent from the formula on the right-hand side. Uniform interpolation has been the focus of significant research activity in Description Logic, with many theoretical results and first implemented systems.

I will not assume any background knowledge about Description Logics but will introduce the relevant notions as required.

An integral part of all debugging activities is the task of fault localization. Most existing fault localization techniques rely on the availability of high quality test suites because they work by comparing failing and passing runs to identify the cause of an error. This limits their applicability. One alternative are techniques that statically analyze an error trace of the program without relying on additional passing runs to compare against. Particularly promising are novel proof-based approaches that leverage the advances in automated theorem proving. These approaches encode error paths into \emph{error trace formulas}. An error trace formula is an unsatisfiable logical formula. A refutation proof of this formula captures the reason why the execution of the error trace fails. By applying an automated theorem prover to obtain such proofs, the relevant portions of the trace can be automatically identified without relying on the availability of test suites. For example, in our previous work, we have used Craig interpolation to extract formulas from the obtained refutation proof. These so-called \emph{error invariants} provide an explanation of the error for a given position in the trace and can be used for more effective static slicing.

In particular, we encode the error trace into a logical formula whose satisfying assignment exactly corresponds to the states that are observed during the concrete execution of the trace. The encoding uses standard symbolic execution techniques. Namely, we first convert the trace into static single-assignment form, then translate each individual statement into a logical constraint, and finally conjoin all the constraints to a single formula. We call the resulting conjunction the \emph{error trace formula} of the trace. By conjoining the error trace formula with the property that is violated at the end of the trace, we obtain an unsatisfiable formula. Since this property is violated at the end of the execution of the error trace, this formula is contradictory (i.e. UNSAT). We then use an interpolating SMT solver to generate an error invariant for each position in the trace from a refutation proof of the unsatisfiable formula. The computed error invariants have two important properties: (1) they are satisfied by the concrete state that is observed at the respective position in the trace; and (2) any execution of the remainder of the trace starting from that position with a state that satisfies the error invariant will still violate the property at the end of the trace.

The generated error invariants are then propagated along the trace to identify maximal subtraces such that the same error invariant holds at both the beginning and the end of the subtrace. From the two properties of error invariants, it follows that the statements between these two positions are irrelevant for understanding the bug and, hence, can be sliced from the trace. We proceed like this for the entire error trace to produce the abstract slice.

While proof-based fault localization techniques are a promising alternative to dynamic techniques, they have practical limitations that have not been addressed in previous work. Precisely capturing the behavior of an erroneous program requires modeling such features as dynamic memory allocation, function calls, inputs, and loops, over traces that can extend to large numbers of instructions. Although mathematical techniques exist to handle these complexities, their implementation in current off-the-shelf theorem provers is often far from robust. For example, heap accesses are traditionally handled using array theories. Unfortunately, most provers lack interpolation procedures for the theory of arrays, making it difficult to automatically infer invariants about heap allocated objects.

To address these shortcomings of purely static approaches, we propose a novel fault localization technique that combines dynamic and static analysis of the error trace. In particular, we note that given an executable error trace, we can determine the concrete value of every variable, and every memory address, using a standard debugger. This information can then be used to dramatically simplify the encoding of the error trace for static analysis. Instead of relying on complex mathematical theories to reason about pointer aliasing, we can directly determine which memory location a pointer references using the debugger. If a trace contains too many statements to analyze using a theorem prover, we can split the trace into subtraces, and use the program states observed during the concrete execution to seed the analysis of the individual subtraces.

We have conducted a case study where we applied our new algorithm to error traces generated from faulty versions of UNIX utils such as gzip and sed. Our case study indicates that our concolic fault localization scales to real-world error traces and generates useful error diagnoses.

Craig interpolation is used in solving bounded model checking (BMC) SAT and SMT problems.

In 2012, Teige et al. succeeded to compute interpolants for stochastic boolean satisfiability problems, i.e. SSAT.

That was achieved by defining sound and complete resolution calculus for SSAT and computing the Craig interpolation for A and B and not S_{A,B}, where not S_{A,B} represents a conflict clause of A and B. Consequently, one can obtain two interpolants for the formula Phi: A and B, where one interpolates A, and the second one interpolates B.

As a result of that, an approach to solve efficiently stochastic bounded model checker problems, e.g. MDPs, was addressed by using SSAT interpolation.

In this work we present a notion of Craig Interpolation for the stochastic modulo theories framework i.e. SSMT.

An SSMT formula consists of free and quantified variables where the latter variables are bound to discrete domains by existential or randomized quantifiers.

In the case of a randomized variable, the variable can be assigned to one of its domain values with a certain probability, where the summation of all probabilities of the same variable has to be one.

The significance of SSMT comes from the fact that one can encode probabilistic hybrid automata problems as SSMT formulae.

Our approach to compute the Craig interpolation for SSMT is as follows: we assume that arithmetic constraints can be relaxed as simple bounds by using interval constraint propagation (ICP) as implemented in iSAT tool. After that, we define a sound and relatively-complete resolution calculus for SSMT formula as done in case of SSAT, such that if a conflict clause is derived with a certain probability, then the latter probability is a safe upper bound of the real satisfaction probability of the SSMT formula. Then we extend P'udlak rules in a way such that simple bounds are treated as literals and if a conflict clause is derived, then we get a generalized Craig interpolation for the whole formula A and B and not S_{A,B}.

Finally, we adapt BMC to the probabilistic case, i.e. PBMC by encoding a step-bounded reachability problems as an SSMT formula, where a generalized Craig interpolation is used to compute an upper bound of the maximum probability of reaching the target states.

Ontologies represented using description logics model domains of interest in terms of concepts and binary relations, and are used in a range of areas including medical science, bio-informatics, semantic web or artificial intelligence. Often, ontologies are large and complex and cover 10,000s of concepts. Uniform interpolants are restricted views of ontologies, that only use a specified set of symbols, while preserving all entailments that can be expressed using these symbols. Uniform interpolation can be used for analysing hidden relations in an ontology, removing confidential concepts from an ontology, computing logical differences between ontologies or extracting specialised ontologies for ontology reuse and has many more applications.

We follow a resolution-based approach to make the computation of uniform interpolants of larger ontologies feasable. Uniform interpolants cannot always be represented finitely in the language of the input ontology, for which situation we offer three solutions: extending the signature with additional concepts, approximating the uniform interpolant, or using fixpoint operators.

Craig interpolation has been recently shown to be useful in a wide variety of problem domains. One use is in strategy extraction for two player games, as described in our accompanying submission. However, interpolation is not without its drawbacks. It is well-known that an interpolant may be very large and highly redundant. Subsequent use of the interpolant requires that it is transformed to CNF or DNF, which will further increase its size.

We present a new approach to handling both the size of interpolants and transformation to clausal representation. Our approach relies on the observation that in many real-world applications, interpolants are defined over a relatively small set of variables. Additionally, in most cases there likely exists a compact representation of the interpolant in CNF. For instance, in our application to games an interpolant represents a set of winning states that is likely to have a simple structure.

We consider the problem of verifying safety of a program in the absence of code for called procedures. Our goal is to synthesize maximal specifications of absent procedures that maintain safety of the given program. This is useful when the software to be verified contains calls to external components (e.g., libraries) that cannot be analyzed. Such components are usually (1) proprietary software whose source code is not available or (2) libraries that are too complex to be analyzed along with the client application. Thus, synthesized specifications can be used as stubs for calls to external components.

In this talk, we discuss a solution to this problem that relies on a reduction to a novel form of logical abduction, which we call generalized abduction. Generalized abduction is a powerful generalization of the classical abduction problem that allows us to abduce an individual specification (formula) for each unknown procedure — as opposed to a single formula in classical abduction. The fact that a procedure may be called from more than one call site, along with the interactions between different call sites, makes this problem quite challenging. We discuss the challenges faced when solving generalized abduction problems, present an algorithm for solving generalized abduction, and outline potential uses of interpolation as a way for solving this problem.

We present a method for interpolation based on DRUP proofs. Interpolants are widely used in model checking, synthesis and other applications. Most interpolation algorithms rely on a a resolution proof produced by a SAT-solver for unsatisfaible formulas. The proof is traversed and translated into an interpolant by replacing resolution steps with AND and OR gates. This process is efficient (once there is a proof) and generates interpolants that are linear in the size of the proof. As this method relies on the existence of a resolution proof, it depends on a SAT-solver that can log a resolution-proof.

In this work, we address three known weakness of this approach, due to its dependence on a resolution proof: (1) performance degradation experienced by the SAT-solver and the extra memory requirements needed when logging a resolution proof; (2) the proof generated by the solver is not necessarily the "best'' proof for interpolantion, and (3) combining proof logging with pre-processing is complicated. We show that these issues can be remedied by using DRUP proofs.

First, we show how to produce an interpolant from a DRUP proof, even when pre-processing is enabled. Then, we give a novel interpolation algorithm that produces interpolants partially in CNF. More precisely, our algorithm returns the CNF component of the interpolant. In case that the proof permits it, the interpolant is a pure CNF. Lastly, we show how a DRUP proof can be reconstructed on-the-fly to yield better interpolants. Our reconstruction aims at maximizing the CNF componenet of the interpolant forcing a specific type of resolutions.

We implemented our DRUP-based interpolation framework in MiniSAT, and evaluated its affect using Avy - a SAT-based model checking algorithm that heavily relies on interpolation. We show the affect our method has on model checking and demonstrate the usefulness of our different heuristics.