Search

Ensuring hardware and software correctness increasingly relies on the use of symbolic logic solvers, in particular for satisfiability modulo theories (SMT). However, building efficient and correct SMT solvers is difficult: even state-of-the-art solvers disagree on instance satisfiability. This work presents a system for witnessing unsatisfiability of instances of NP problems, commonly appearing in verification, in a way that is natural to SMT solving. Our implementation of the system seems to often result in significantly smaller witnesses, lower solving overhead, and faster checking time in comparison to existing proof formats that can serve a similar purpose.

Satisfiability Modulo Theories (SMT) is an extension of the propositional satisfiability problem (SAT) to other, well-chosen (first-order) theories such as integers, reals, and bit-vectors. This approach currently enjoys much popularity, especially in the field of software verification, where SMT solvers have become the de facto standard tool for the discharge of verification conditions. The development of parallel SMT solvers is still in its infancy, but the first general paradigms have been established. This chapter provides an overview of the recent advances in this area, specifically algorithm portfolio, search-space partitioning, and problem decomposition techniques, and how they relate to each other in theory and practice.

Interpolating, i.e., computing safe over-approximations for a system represented by a logical formula, is at the core of symbolic model-checking. One of the central tools in modeling programs is the use of the equality logic and uninterpreted functions (EUF), but certain aspects of its interpolation, such as size and the logical strength, are still relatively little studied. In this paper we present a solid framework for building compact, strength-controlled interpolants, prove its strength and size properties on EUF, implement and combine it with a propositional interpolation system and integrate the implementation into a model checker. We report encouraging results on using the interpolants both in a controlled setting and in the model checker. Based on the experimentation the presented techniques have potentially a big impact on the final interpolant size and the number of counter-example-guided refinements.

Property Directed Reachability (PDR) is an efficient model checking technique. However, the intrinsic high computational complexity prevents PDR from meeting the challenges of real world verification. To address this problem, this paper introduces the parallel algorithm P3 based on: 1) partitioning of the input problem, 2) exchanging of learned reachability information, and 3) using algorithm portfolios. The generic nature of the proposed techniques makes them immediately suitable for software verification. This paper investigates the benefits of these techniques while taken individually and when combined together, implemented using distributed computing environment on top of the SMT-based software model checker Spacer. In our experiments over SV-COMP benchmarks we observe up to an order of magnitude speedup with respect to the sequential implementation with twice as many instances solved within a timeout.

This paper studies the following question: given an instance of the propositional satisfiability problem, a randomized satisfiability solver, and a cluster of n computers, what is the best way to use the computers to solve the instance? Two approaches, simple distribution and search space partitioning as well as their combinations are investigated both analytically and empirically. It is shown that the results depend heavily on the type of the problem (unsatisfiable, satisfiable with few solutions, and satisfiable with many solutions) as well as on how good the search space partitioning function is. In addition, the behavior of a real search space partitioning function is evaluated in the same framework. The results suggest that in practice one should combine the simple distribution and search space partitioning approaches.

Computational Grids provide a widely distributed computing environment suitable for randomized SAT solving. This paper develops techniques for incorporating clause learning, known to yield significant speed-ups in the sequential case, in such a distributed framework. The approach exploits existing state-of-the-art clause learning SAT solvers by embedding them with virtually no modifications. The paper presents an algorithmic framework for learning-enhanced randomized SAT solving in Grid environments. With a substantial amount of controlled experiments it is demonstrated that this approach enables a form of clause learning which is not directly available in the underlying sequential SAT solver. Finally, an implementation of the algorithm is run in a production level Grid where it solves several problems not solved in the SAT 2007 solver competition.

Two of the static analysis techniques presented in this book use Craig interpolation, a means of over-approximation, to achieve efficient SAT-based symbolic model checking. Different verification applications exploit interpolants for different purposes; it is unlikely that a single interpolation procedure could provide interpolants fit for all cases. This chapter describes the PeRIPLO framework, an interpolating SAT solver that implements a set of techniques to generate and manipulate interpolants for different model-checking tasks. Even though the PeRIPLO framework can be used for many other purposes besides static analysis, we will use it to illustrate in an interesting way the benefits and challenges of Craig-interpolation-based Bounded Model Checking. We demonstrate the flexibility of the framework in two software bounded model checking applications described in Chaps. 5 and 6: verification of a given source code incrementally with respect to various properties, and verification of software upgrades with respect to a fixed set of properties. Both applications use interpolation for generating function summaries. Our systematic experimental investigation shows that the size and logical strength of interpolants significantly affect verification, and that these characteristics depend on the role interpolants play in the verification process. The chapter is based on the research previously published in [RAF+13].

In this chapter we present Verification-Aided Regression Testing, a novel extension of regression testing that is significantly less sensitive to the completeness of the validation test suite due to the use of model checking. We extend the use of test case executions from conventional direct fault discovery to generation of behavioral properties specific to the new version by (i) automatically producing properties that are proved to hold for the base version of a program, (ii) automatically identifying and checking on the upgraded program only the properties that, according to the developers’ intention, must be preserved by the upgrade, and (iii) reporting the faults and the corresponding counterexamples that are not revealed by the regression tests. Our empirical study on both open-source and industrial software systems show that Verification-Aided Regression Testing produces properties that can be extremely beneficial in increasing the effectiveness of regression testing by timely and automatically detecting faults unnoticed by existing test suites.

Verification based on model checking has recently obtained an important role in certain software engineering tasks, such as developing operating system device drivers. This extended abstract discusses how model checking can be made more efficient by using the structure from program function calls. We use this idea in two orthogonal ways, both of which fundamentally depend on automatically summarizing the relevant behavior of the function calls based on an earlier verification. The first approach assumes a piece of software needs to be verified with respect to a set of properties, whereas the second approach considers a case where an early version of a software has been verified but needs to be re-verified after an upgrade. These techniques have been implemented in tools FunFrog and eVolCheck for verifying C programs. Both of them have been tested on a range of academic and industrial benchmarks, and provide in many cases an order of magnitude speed-up with respect to the baseline. They seem to scale to programs with thousands of lines of code.

Propositional interpolation is widely used as a means of overapproximation to achieve efficient SAT-based symbolic model checking. Different verification applications exploit interpolants for different purposes; it is unlikely that a single interpolation procedure could provide interpolants fit for all cases. This paper describes the PeRIPLO framework, an interpolating SAT-solver that implements a set of techniques to generate and manipulate interpolants for different model checking tasks. We demonstrate the flexibility of the framework in two software bounded model checking applications: verification of a given source code incrementally with respect to various properties, and verification of software upgrades with respect to a fixed set of properties. Both applications use interpolation for generating function summaries. Our systematic experimental investigation shows that size and logical strength of interpolants significantly affect verification, that these characteristics depend on the role played by interpolants, and that therefore techniques for tuning size and strength can be used to customize interpolants in different applications.

Solving instances of the propositional satisfiability problem (SAT) in parallel has received a significant amount of attention as the number of cores in a typical workstation is steadily increasing. With the increase of the number of cores, in particular the scalability of such approaches becomes essential for fully harnessing the potential of modern architectures. The best parallel SAT solvers have, until recently, been based on algorithm portfolios, while search-space partitioning approaches have been less successful. We prove, under certain natural assumptions on the partitioning function, that search-space partitioning can always result in an increased expected run time, justifying the success of the portfolio approaches. Furthermore, we give first controlled experiments showing that an approach combining elements from partitioning and portfolios scales better than either of the two approaches and succeeds in solving instances not solved in a recent solver competition.

This work studies the solving of challenging SAT problem instances in distributed computing environments that have massive amounts of parallel resources but place limits on individual computations. We present an abstract framework which extends a previously presented iterative partitioning approach with clause learning, a key technique applied in modern SAT solvers. In addition we present two techniques that alter the clause learning of modern SAT solvers to fit the framework. An implementation of the proposed framework is then analyzed experimentally using a well-known set of benchmark instances. The results are very encouraging. For example, the implementation is able to solve challenging SAT instances not solvable in reasonable time by state-of-the-art sequential and parallel SAT solvers.

In this paper we study the problem of solving hard propositional satisfiability problem (SAT) instances in a computing grid or cloud, where run times and communication between parallel running computations are limited. We study analytically an approach where the instance is partitioned iteratively into a tree of subproblems and each node in the tree is solved in parallel. We present new methods for constructing partitions which combine clause learning and lookahead. The methods are incorporated into the iterative approach and its performance is demonstrated with an extensive comparison against the best sequential solvers in the SAT competition 2009 as well as against two efficient parallel solvers.

This paper studies the following question: given an instance of the propositional satisfiability problem, a randomized satisfiability solver, and a cluster of n computers, what is the best way to use the computers to solve the instance? Two approaches, simple distribution and search space partitioning as well as their combinations are investigated both analytically and empirically. It is shown that the results depend heavily on the type of the problem (unsatisfiable, satisfiable with few solutions, and satisfiable with many solutions) as well as on how good the search space partitioning function is. In addition, the behavior of a real search space partitioning function is evaluated in the same framework. The results suggest that in practice one should combine the simple distribution and search space partitioning approaches.

Computational Grids provide a widely distributed computing environment suitable for randomized SAT solving. This paper develops techniques for incorporating learning, known to yield significant speed-ups in the sequential case, in such a distributed framework. The approach exploits existing state-of-the-art clause learning SAT solvers by embedding them with virtually no modifications. We show that for many industrial SAT instances, the expected run time can be decreased by carefully combining the learned clauses from the distributed solvers. We compare different parallel learning strategies by using a representative set of benchmarks, and exploit the results to devise an algorithm for learning-enhanced randomized SAT solving in Grid environments. Finally, we experiment with an implementation of the algorithm in a production level Grid and solve several problems which were not solved in the SAT 2007 solver competition.

Grid computing offers a promising approach to solving challenging computational problems in an environment consisting of a large number of easily accessible resources. In this paper we develop strategies for solving collections of hard instances of the propositional satisfiability problem (SAT) with a randomized SAT solver run in a Grid. We study alternative strategies by using a simulation framework which is composed of (i) a grid model capturing the communication and management delays, and (ii) run-time distributions of a randomized solver, obtained by running a state-of-the-art SAT solver on a collection of hard instances. The results are experimentally validated in a production level Grid. When solving a single hard SAT instance, the results show that in practice only a relatively small amount of parallelism can be efficiently used; the speedup obtained by increasing parallelism thereafter is negligible. This observation leads to a novel strategy of using grid to solve collections of hard instances. Instead of solving instances one-by-one, the strategy aims at decreasing the overall solution time by applying an alternating distribution schedule.

In this paper we show how grid computing can be used to improve the operation of a medical image search system. The paper introduces the basic principles of a content-based image retrieval (CBIR) system and identifies the computationally challenging tasks in the system. For the computationally challenging tasks an efficient design is proposed that uses distributed grid computing to carry out the image processing in a distributed and efficient way. The algorithms of the search system are executed by using a real medical image collection as input and a grid computing infrastructure to provide the needed computing power. Finally, the results show how the image processing task that required tens of hours to complete can be processed by using only a fraction of the originally required computing time.