Abstract Many digital systems are designed as collections of asynchronous processes orchestrated by a domain-specific scheduler. The verification of such scheduler-restricted asynchronous systems (SRA) is challenging due to process-process and process-scheduler interactions. In this paper, we tackle the problem of verifying configurable SRA. A configurable SRA describes an unbounded family of possible SRA, each resulting from an instantiation satisfying given configuration constraints; our goal is proving at once that every legal instantiation of a configurable SRA is correct. We propose a contract-based, deductive verification approach that combines (i) compositional proof rules that abstract the scheduler to prove top-level invariant properties, (ii) automatic summarizations of the methods invoked by the scheduler, (iii) simplification with respect to the nature of the space of configurations. The approach is grounded in (object-oriented) first order logic, requires reasoning over quantified statements, and leverages the Dafny software verifier as a backend. An experimental evaluation on industrial case studies demonstrates that the framework scales effectively and enables practical reasoning about complex parameterized behaviors.

Abstract In the field of formal verification, certifying proofs serve as compelling evidence to demonstrate the correctness of a model within a deductive system. These proofs can be automatically generated as a by-product of the verification process and are key artifacts for high-assurance systems. Their significance lies in their ability to be independently verified by proof checkers, which provides a more convenient approach than certifying the tools that generate them. Modern model checking algorithms adopt deductive methods and usually generate proofs in terms of inductive invariants, assuming that these apply to the original system under verification. Model checkers, though, often make use of a range of complex pre-processing simplifications and transformations to ease the verification process, which add another layer of complexity to the generation of proofs. In this paper, we present a novel approach for certifying model checking results exploiting a theorem prover and a theory of temporal deductive rules that can support various kinds of transformations and simplification of the original circuit. We implemented and experimentally evaluated our contribution on invariants generated using two state-of-the-art model checkers, nuXmv and PdTRAV, and by defining a set of rules within a theorem prover, to validate each certificate.

Abstract In this paper we describe an industrial experience in the verification of the logic of a Railway Protection System (RPS). The RPS is designed within AIDA, a structured model-based design workflow and toolset. The RPS is written in a domain specific language amenable to signaling engineers, that is converted into Extended Finite State Machines (EFSM), and then into executable code. The RPS is parameterized, i.e., it can be applied, after configuration, in different operational scenarios. The logic is divided in classes, that are instantiated depending on the specific application. The verification challenge is to ensure that the required properties hold for all possible instantiations . We follow a verification approach based on the use of deductive methods, leveraging the Dafny framework. The AIDA environment is used to translate the RPS logic into Dafny, and also to automatically generate the contracts summarizing the methods implementing the guards and effects of the EFSM transitions. This approach greatly limits the need for human interaction with the underlying Dafny proof engine. In addition to domain specific optimizations, it results in an automated and efficient proof of the RPS properties.

Abstract is a recently-proposed SAT-based liveness model checking algorithm that showed remarkable performance compared to other state-of-the-art approaches, both in absolute terms (solving more problems overall than other engines on standard benchmark sets) as well as in relative terms (solving several problems that none of the other engines could solve). proves or disproves properties of the form FGq , by trying to show that $$\lnot q$$ ¬ q can be visited only a finite number of times via an incremental reduction to a sequence of reachability queries. A key factor in the good performance of is the extraction of “shoals” from the inductive invariants of the reachability queries to block states that can reach $$\lnot q$$ ¬ q a bounded number of times. In this paper, we generalize to handle infinite-state systems, using the Verification Modulo Theories paradigm. In contrast to the finite-state case, liveness cannot be simply reduced to finding a bound on the number of occurrences of $$\lnot q$$ ¬ q on paths. We propose therefore a solution leveraging predicate abstraction and termination techniques based on well-founded relations. In particular, we show how we can extract shoals that take into account the well-founded relations. We implemented the technique on top of the open source VMT engine IC3ia and we experimentally demonstrate how the new extension maintains the performance advantages (both absolute and relative) of the original , thus significantly contributing to advancing the state of the art of infinite-state liveness verification.

Abstract We present , a new SAT-based model-checking algorithm for the verification of liveness properties of finite-state symbolic transition systems. Like other recent approaches, works by reducing liveness checking to a sequence of safety checks. Similarly to , it incrementally strengthens the input system using constraints obtained by refuting candidate counterexamples to the input liveness property, assumed (w.l.o.g.) to be of the form FGq. Differently from (and crucially), however, instead of directly searching for lasso-shaped counterexamples visiting $$\lnot q$$ ¬ q infinitely-often, searches for counterexamples incrementally, via a recursive chain of safety checks, each of which tries to determine whether it is possible to reach a $$\lnot q$$ ¬ q -state from a given $$\lnot q$$ ¬ q -state (which was previously determined to be reachable), in a manner similar to . When the current candidate counterexample is refuted, exploits the inductive invariants generated by the (recursive) safety checks to restrict the search space, until either no more reachable $$\lnot q$$ ¬ q -states remain, or a real lasso-shaped counterexample is found. In this paper, we describe in detail, prove its soundness and completeness, and compare it against the state of the art both theoretically and empirically. Our experimental results show that our implementation of outperforms state-of-the-art implementations of , and other SAT-based liveness checking algorithms on a wide range of benchmarks from the literature.

Abstract Automated driving functions are among the most critical software components to develop. Before deployment in series vehicles, it has to be shown that the functions drive safely and in compliance with traffic rules. Despite the coverage that can be reached with very large amounts of test drives, corner cases remain possible. Furthermore, the development is subject to time-to-delivery constraints due to the highly competitive market, and potential logical errors must be found as early as possible. We describe an approach to improve the development of an actual industrial behavior planner for the Automated Driving Alliance between Bosch and Cariad. The original process landscape for verification and validation is extended with model checking techniques. The idea is to integrate automated extraction mechanisms that, starting from the C++ code of the planner, generate a higher-level model of the underlying logic. This model, composed in closed loop with expressive environment descriptions, can be exhaustively analyzed with model checking. This results, in case of violations, in traces that can be re-executed in system simulators to guide the search for errors. The approach was exemplarily deployed in series development, and successfully found relevant issues in intermediate versions of the planner at development time.

This article addresses the problem of checking invariant properties for a large class of symbolic transition systems defined by a combination of SMT theories and quantifiers. State variables can be functions from an uninterpreted sort (finite but unbounded) to an interpreted sort, such as the integers under the theory of linear arithmetic. This formalism is very expressive and can be used for modeling parameterized systems, array-manipulating programs, and more. We propose two algorithms for finding universal inductive invariants for such systems. The first algorithm combines an IC3-style loop with a form of implicit predicate abstraction to construct an invariant in an incremental manner. The second algorithm constructs an under-approximation of the original problem and searches for a formula which is an inductive invariant for this case; then, the invariant is generalized to the original case and checked with a portfolio of techniques. We have implemented the two algorithms and conducted an extensive experimental evaluation, considering various benchmarks and different tools from the literature. As far as we know, our method is the first capable of handling in a large class of systems in a uniform way. The experiment shows that both algorithms are competitive with the state of the art.

Abstract This paper describes , a tool for the verification of imperative programs. operates on an intermediate verification language called , with a formally-specified semantics based on smt, allowing the specification of both reachability and liveness properties. It integrates several state-of-the-art verification engines based on sat and smt. Moreover, it provides additional functionalities such as a flexible Python api, a customizable C front-end, generation of counterexamples, support for simulation and symbolic execution, and translation into multiple low-level verification formalisms. Our experimental analysis shows that is competitive with state-of-the-art software verifiers on a large range of programs. Thanks to its flexibility, has already been used in various industrial projects and academic publications, both as a verification back-end and as a benchmark generator.

Abstract / and its variants have been the prominent approaches to safety model checking in recent years. Compared to the previous model-checking algorithms like (Bounded Model Checking) and (Interpolation Model Checking), / is attractive due to its completeness (vs. ) and scalability (vs. ). / maintains an over-approximate state sequence for proving the correctness. Although the sequence refinement methodology is known to be crucial for performance, the literature lacks a systematic analysis of the problem. We propose an approach based on the definition of i- good lemmas, and the introduction of two kinds of heuristics, i.e., and , to steer the search towards the construction of $$i$$ -good lemmas. The approach is applicable to and its variant (Complementary Approximate Reachability), and it is very easy to integrate within existing systems. We implemented the heuristics into two open-source model checkers, and , as well as into the mature platform, and carried out an extensive experimental evaluation on HWMCC benchmarks. The results show that the proposed heuristics can effectively compute more $$i$$ -good lemmas, and thus improve the performance of all the above checkers.

Abstract We present , a framework for the integration of modern verification tools in the context of AUTOSAR, a widely-used open standard for the development of automotive software systems. Our framework enables the automatic end-to-end verification of system-level properties using a compositional approach. It combines software model checking techniques for the verification of software components at the code level with a contract-based analysis for verifying their correct composition. In this paper, we present the tool through its application on a representative automotive case study, discussing the main functionalities provided and the results obtained.

Analysis models, technologies and tools are extensively used in the automotive domain to validate and optimize the design and implementation of SW systems. This is especially true for modern systems including advanced autonomous (and complex) features. The range of analysis methods that can be applied is extremely wide and goes from functional correctness to functional safety to timing (and schedulability), security, and possibly even more. The AUTOSAR automotive standard has been defined with the purpose of standardizing the SW architecture of automotive systems and enable the construction of systems by composing SW components that are portable and abstract with respect to the underlying HW/SW platform. However, AUTOSAR was originally developed with portability of code in mind, and even if it quickly evolved to include a system-level modeling language (with its metamodel) and later extensions to deal with the needs of analysis methods (and tools), it is hardly comprehensive and still affected by several omissions and limitations. To fix the limitations with respect to timing and schedulability analysis Bosch developed the Amalthea (later App4MC) metamodel and tools. In Huawei, a more general (and ambitious) approach was undertaken to support not only timing analysis, but also model checking (or other types of formal verification), safety analysis and even design optimization. The approach is based on the concepts of a unified (modular) metamodel and a framework based on Eclipse to integrate analysis methods and tools. In this paper we describe the framework and the results obtained with respect to the objectives of functional verification and timing analysis.

Abstract Many safety critical systems guarantee fault-tolerance by using several redundant copies of their components. When designing such redundancy architectures, it is crucial to analyze their fault trees, which describe combinations of faults of individual components that may cause malfunction of the system. State-of-the-art techniques for fault tree computation use first-order formulas with uninterpreted functions to model the transformations of signals performed by the redundancy system and an AllSMT query for computation of the fault tree from this encoding. Scalability of the analysis can be further improved by techniques such as predicate abstraction, which reduces the problem to Boolean case. In this paper, we show that as far as fault trees of redundancy architectures are concerned, signal transformation can be equivalently viewed in a purely Boolean way as fault propagation. This alternative view has important practical consequences. First, it applies also to general redundancy architectures with cyclic dependencies among components, to which the current state-of-the-art methods based on AllSMT are not applicable, and which currently require expensive sequential reasoning. Second, it allows for a simpler encoding of the problem and usage of efficient algorithms for analysis of fault propagation, which can significantly improve the runtime of the analyses. A thorough experimental evaluation demonstrates the superiority of the proposed techniques.

Abstract In this paper, we consider the problem of model checking fair transition systems expressed symbolically in the framework of Satisfiability Modulo Theories. This problem, referred to as Verification Modulo Theories, is tackled by combining two key elements from the legacy of Ed Clarke: SAT-based verification and abstraction refinement. We show how fundamental SAT-based algorithms have been lifted to deal with the extended expressiveness with a tight integration of abstraction within a CEGAR loop. In turn, the case of nonlinear theories is based on a CEGAR loop over the linear case. These two elements have also deeply impacted the development of the NuSMV model checker, born from a joint project between FBK and CMU, and its successor nuXmv, whose core integrates SMT-based techniques for VMT.

We develop a framework for model checking infinite-state systems by automatically augmenting them with auxiliary variables, enabling quantifier-free induction proofs for systems that would otherwise require quantified invariants. We combine this mechanism with a counterexample-guided abstraction refinement scheme for the theory of arrays. Our framework can thus, in many cases, reduce inductive reasoning with quantifiers and arrays to quantifier-free and array-free reasoning. We evaluate the approach on a wide set of benchmarks from the literature. The results show that our implementation often outperforms state-of-the-art tools, demonstrating its practical potential.

Abstract The problem of invariant checking in parametric systems – which are required to operate correctly regardless of the number and connections of their components – is gaining increasing importance in various sectors, such as communication protocols and control software. Such systems are typically modeled using quantified formulae, describing the behaviour of an unbounded number of (identical) components, and their automatic verification often relies on the use of decidable fragments of first-order logic in order to effectively deal with the challenges of quantified reasoning. In this paper, we propose a fully automatic technique for invariant checking of parametric systems which does not rely on quantified reasoning. Parametric systems are modeled with array-based transition systems, and our method iteratively constructs a quantifier-free abstraction by analyzing, with SMT-based invariant checking algorithms for non-parametric systems, increasingly-larger finite instances of the parametric system. Depending on the verification result in the concrete instance, the abstraction is automatically refined by leveraging canditate lemmas from inductive invariants, or by discarding previously computed lemmas. We implemented the method using a quantifier-free SMT-based IC3 as underlying verification engine. Our experimental evaluation demonstrates that the approach is competitive with the state of the art, solving several benchmarks that are out of reach for other tools.

Abstract The process of developing civil aircraft and their related systems includes multiple phases of Preliminary Safety Assessment (PSA). An objective of PSA is to link the classification of failure conditions and effects (produced in the functional hazard analysis phases) to appropriate safety requirements for elements in the aircraft architecture. A complete and correct preliminary safety assessment phase avoids potentially costly revisions to the design late in the design process. Hence, automated ways to support PSA are an important challenge in modern aircraft design. A modern approach to conducting PSAs is via the use of abstract propagation models, that are basically hyper-graphs where arcs model the dependency among components, e.g. how the degradation of one component may lead to the degraded or failed operation of another. Such models are used for computingfailure propagations: the fault of a component may have multiple ramifications within the system, causing the malfunction of several interconnected components. A central aspect of this problem is that of identifying the minimal fault combinations, also referred to asminimal cut sets, that cause overall failures. In this paper we propose an expressive framework to model failure propagation, catering for multiple levels of degradation as well as cyclic and nondeterministic dependencies. We define a formal sequential semantics, and present an efficient SMT-based method for the analysis of failure propagation, able to enumerate cut sets that are minimal with respect to the order between levels of degradation. In contrast with the state of the art, the proposed approach is provably more expressive, and dramatically outperforms other systems when a comparison is possible.

Abstract Semi-algebraic abstraction is an approach to the safety verification problem for polynomial dynamical systems where the state space is partitioned according to the sign of a set of polynomials. Similarly to predicate abstraction for discrete systems, the number of abstract states is exponential in the number of polynomials. Hence, semi-algebraic abstraction is expensive to explicitly compute and then analyze (e.g., to prove a safety property or extract invariants). In this paper, we propose an implicit encoding of the semi-algebraic abstraction, which avoids the explicit enumeration of the abstract states: the safety verification problem for dynamical systems is reduced to a corresponding problem for infinite-state transition systems, allowing us to reuse existing model-checking tools based on Satisfiability Modulo Theory (SMT). The main challenge we solve is to express the semi-algebraic abstraction as a first-order logic formula that is linear in the number of predicates, instead of exponential, thus letting the model checker lazily explore the exponential number of abstract states with symbolic techniques. We implemented the approach and validated experimentally its potential to prove safety for polynomial dynamical systems.

Abstract We develop a framework for model checking infinite-state systems by automatically augmenting them with auxiliary variables, enabling quantifier-free induction proofs for systems that would otherwise require quantified invariants. We combine this mechanism with a counterexample-guided abstraction refinement scheme for the theory of arrays. Our framework can thus, in many cases, reduce inductive reasoning with quantifiers and arrays to quantifier-free and array-free reasoning. We evaluate the approach on a wide set of benchmarks from the literature. The results show that our implementation often outperforms state-of-the-art tools, demonstrating its practical potential.

In this paper, we propose to extend First-Order Linear-time Temporal Logic with Past adding two operators “at next” and “at last”, which take in input a term and a formula and return the value of the term at the next state in the future or last state in the past in which the formula holds. The new logic, named LTL-EF, can be interpreted with different models of time (including discrete, dense, and super-dense time) and with different first-order theories (à la Satisfiability Modulo Theories (SMT)). We show that the “at next” and “at last” can encode (first-order) MTL0,∞with counting. We provide rewriting procedures to reduce the satisfiability problem to the discrete-time case (to leverage on the mature state-of-the-art corresponding verification techniques) and to remove the extra functional symbols. We implemented these techniques in thenuXmvmodel checker enabling the analysis of LTL-EFand MTL0,∞based on SMT-based model checking. We show the feasibility of the approach experimenting with several non-trivial valid and satisfiable formulas.

nuXmv is a well-known symbolic model checker, which implements various state-of-the-art algorithms for the analysis of finite- and infinite-state transition systems and temporal logics. In this paper, we present a new version that supports timed systems and logics over continuous super-dense semantics. The system specification was extended with clocks to constrain the timed evolution. The support for temporal properties has been expanded to include $$\textsc {MTL}_{0,\infty }$$ formulas with parametric intervals. The analysis is performed via a reduction to verification problems in the discrete-time case. The internal representation of traces has been extended to go beyond the lasso-shaped form, to take into account the possible divergence of clocks. We evaluated the new features by comparing nuXmv with other verification tools for timed automata and $$\textsc {MTL}_{0,\infty }$$ , considering different benchmarks from the literature. The results show that nuXmv is competitive with and in many cases performs better than state-of-the-art tools, especially on validity problems for $$\textsc {MTL}_{0,\infty }$$ .

In the context of formal verification, certifying proofs are proofs of the correctness of a model in a deduction system produced automatically as outcome of the verification. They are quite appealing for high-assurance systems because they can be verified independently by proof checkers, which are usually simpler to certify than the proof-generating tools. Model checking is one of the most prominent approaches to formal verification of temporal properties and is based on an algorithmic search of the system state space. Although modern algorithms integrate deductive methods, the generation of proofs is typically restricted to invariant properties only. In this paper, we solve this issue in the context of Linear-time Temporal Logic. By exploiting the k-liveness algorithm, we show how to extend proof generation capabilities for invariant checking to cover full LTL properties, in a simple and efficient manner, with essentially no overhead for the model checker. We implemented the technique on top of an IC3 engine, and show the feasibility of the approach on a variety of benchmarks.

Symbolic execution systematically explores program paths by solving path conditions --- formulas over symbolic variables. Typically, the symbolic variables range over numbers, arrays and strings. We introduce symbolic execution with existential second-order constraints --- an extension of traditional symbolic execution that allows symbolic variables to range over functions whose interpretations are restricted by a user-defined language. The aims of this new technique are twofold. First, it offers a general analysis framework that can be applied in multiple domains such as program repair and library modelling. Secondly, it addresses the path explosion problem of traditional first-order symbolic execution in certain applications. To realize this technique, we integrate symbolic execution with program synthesis. Specifically, we propose a method of second-order constraint solving that provides efficient proofs of unsatisfiability, which is critical for the performance of symbolic execution. Our evaluation shows that the proposed technique (1) helps to repair programs with loops by mitigating the path explosion, (2) can enable analysis of applications written against unavailable libraries by modelling these libraries from the usage context.

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some theory or combination of theories; Verification Modulo Theories (VMT) is the problem of analyzing the reachability for transition systems represented in terms of SMT formulae. In this article, we tackle the problems of SMT and VMT over the theories of nonlinear arithmetic over the reals (NRA) and of NRA augmented with transcendental (exponential and trigonometric) functions (NTA). We propose a new abstraction-refinement approach for SMT and VMT on NRA or NTA, called Incremental Linearization . The idea is to abstract nonlinear multiplication and transcendental functions as uninterpreted functions in an abstract space limited to linear arithmetic on the rationals with uninterpreted functions. The uninterpreted functions are incrementally axiomatized by means of upper- and lower-bounding piecewise-linear constraints. In the case of transcendental functions, particular care is required to ensure the soundness of the abstraction. The method has been implemented in the M ath SAT SMT solver and in the nu X mv model checker. An extensive experimental evaluation on a wide set of benchmarks from verification and mathematics demonstrates the generality and the effectiveness of our approach.

IC3 is one of the most successful algorithms for hardware model checking. Since its invention in 2010, several variants of the original algorithm have been published, proposing optimizations and/or alternative procedures for many different steps of the algorithm. In this paper, we present a thorough empirical comparison of a large set of optimizations and procedures for the steps of IC3, considering “high-level” variants/extensions to the basic algorithm, as well as “low-level” optimizations/configuration settings. We implemented each of them in the same tool, optimizing the implementations to the best of our knowledge. This enabled for a flexible experimentation in a controlled environment, and to gain new insights about their most important differences and commonalities, as well as about their performance characteristics. We conducted the experiments using as benchmarks the problems used in the last four editions of the hardware model checking competition. The analysis helped us to identify several settings leading to significant improvements with respect to a basic implementation of IC3.

Designers are often required to explore alternative solutions, trading off along different dimensions (e.g., power consumption, weight, cost, reliability, response time). Such exploration can be encoded as a problem of parameter synthesis, i.e., finding a parameter valuation (representing a design solution) such that the corresponding system satisfies a desired property. In this paper, we tackle the problem of parameter synthesis with multi-dimensional cost functions by finding solutions that are in the Pareto front: in the space of best trade-offs possible. We propose several algorithms, based on IC3, that interleave in various ways the search for parameter valuations that satisfy the property, and the optimization with respect to costs. The most effective one relies on the reuse of inductive invariants and on the extraction of unsatisfiable cores to accelerate convergence. Our experimental evaluation shows the feasibility of the approach on practical benchmarks from diagnosability synthesis and product-line engineering, and demonstrates the importance of a tight integration between model checking and cost optimization.

We present a bit-precise decision procedure for the theory of floating-point arithmetic. The core of our approach is a non-trivial, lattice-theoretic generalisation of the conflict-driven clause learning algorithm in modern sat solvers to lattice-based abstractions. We use floating-point intervals to reason about the ranges of variables, which allows us to directly handle arithmetic and is more efficient than encoding a formula as a bit-vector as in current floating-point solvers. Interval reasoning alone is incomplete, and we obtain completeness by developing a conflict analysis algorithm that reasons natively about intervals. We have implemented this method in the mathsat5 smt solver and evaluated it on assertion checking problems that bound the values of program variables. Our new technique is faster than a bit-vector encoding approach on 80 % of the benchmarks, and is faster by one order of magnitude or more on 60 % of the benchmarks. The generalisation of cdcl we propose is widely applicable and can be used to derive abstraction-based smt solvers for other theories.

The problem of finding small unsatisfiable cores for SAT formulas has recently received a lot of interest, mostly for its applications in formal verification. However, propositional logic is often not expressive enough for representing many interesting verification problems, which can be more naturally addressed in the framework of Satisfiability Modulo Theories, SMT. Surprisingly, the problem of finding unsatisfiable cores in SMT has received very little attention in the literature. In this paper we present a novel approach to this problem, called the Lemma-Lifting approach. The main idea is to combine an SMT solver with an external propositional core extractor. The SMT solver produces the theory lemmas found during the search, dynamically lifting the suitable amount of theory information to the Boolean level. The core extractor is then called on the Boolean abstraction of the original SMT problem and of the theory lemmas. This results in an unsatisfiable core for the original SMT problem, once the remaining theory lemmas are removed. The approach is conceptually interesting, and has several advantages in practice. In fact, it is extremely simple to implement and to update, and it can be interfaced with every propositional core extractor in a plug-and-play manner, so as to benefit for free of all unsat-core reduction techniques which have been or will be made available. We have evaluated our algorithm with a very extensive empirical test on SMT-LIB benchmarks, which confirms the validity and potential of this approach.

We address the problem of computing the exact abstraction of a program with respect to a given set of predicates, a key computation step in Counter-Example Guided Abstraction Refinement. We build on a recently proposed approach that integrates BDD-based quantification techniques with SMT-based constraint solving to compute the abstraction. We extend the previous work in three main directions. First, we propose a much tighter integration of the BDD-based and SMT-based reasoning where the two solvers strongly collaborate to guide the search. Second, we propose a technique to reduce redundancy in the search by blocking already visited models. Third, we present an algorithm exploiting a conjunctively partitioned representation of the formula to quantify. This algorithm provides a general framework where all the presented optimizations integrate in a natural way. Moreover, it allows to overcome the limitations of the original approach that used a monolithic BDD representation of the formula to quantify. We experimentally evaluate the merits of the proposed optimizations, and show how they allow to significantly improve over previous approaches.

The problem of computing Craig interpolants has recently received a lot of interest. In this article, we address the problem of efficient generation of interpolants for some important fragments of first-order logic, which are amenable for effective decision procedures, called satisfiability modulo theory (SMT) solvers. We make the following contributions. First, we provide interpolation procedures for several basic theories of interest: the theories of linear arithmetic over the rationals, difference logic over rationals and integers, and UTVPI over rationals and integers. Second, we define a novel approach to interpolate combinations of theories that applies to the delayed theory combination approach. Efficiency is ensured by the fact that the proposed interpolation algorithms extend state-of-the-art algorithms for satisfiability modulo theories. Our experimental evaluation shows that the MathSAT SMT solver can produce interpolants with minor overhead in search, and much more efficiently than other competitor solvers.

Several successful approaches to software verification are based on the construction and analysis of an abstract reachability tree (ART). The ART represents unwindings of the control-flow graph of the program. Traditionally, a transition of the ART represents a single block of the program, and therefore, we call this approach single-block encoding (SBE). SBE may result in a huge number of program paths to be explored, which constitutes a fundamental source of inefficiency. We propose a generalization of the approach, in which transitions of the ART represent larger portions of the program; we call this approach large-block encoding (LBE). LBE may reduce the number of paths to be explored up to exponentially. Within this framework, we also investigate symbolic representations: for representing abstract states, in addition to conjunctions as used in SBE, we investigate the use of arbitrary Boolean formulas; for computing abstract-successor states, in addition to Cartesian predicate abstraction as used in SBE, we investigate the use of Boolean predicate abstraction. The new encoding leverages the efficiency of state-of-the-art SMT solvers, which can symbolically compute abstract large-block successors. Our experiments on benchmark C programs show that the large-block encoding outperforms the single-block encoding.