Catálogo de publicaciones - libros

In this paper we present a new decision procedure for the satisfiability of Linear Arithmetic Logic (LAL), i.e. boolean combinations of propositional variables and linear constraints over numerical variables. Our approach is based on the well known integration of a propositional SAT procedure with theory deciders, enhanced in the following ways.

First, our procedure relies on an solver for linear arithmetic, that is able to exploit the fact that it is repeatedly called to analyze sequences of increasingly large sets of constraints. Reasoning in the theory of LA interacts with the boolean top level by means of a stack-based interface, that enables the top level to add constraints, set points of backtracking, and backjump, without restarting the procedure from scratch at every call. Sets of inconsistent constraints are found and used to drive backjumping and learning at the boolean level, and theory atoms that are consequences of the current partial assignment are inferred.

Second, the solver is : a satisfying assignment is constructed by reasoning at different levels of abstractions (logic of equality, real values, and integer solutions). Cheaper, more abstract solvers are called first, and unsatisfiability at higher levels is used to prune the search. In addition, theory reasoning is partitioned in different clusters, and tightly integrated with boolean reasoning.

We demonstrate the effectiveness of our approach by means of a thorough experimental evaluation: our approach is competitive with and often superior to several state-of-the-art decision procedures.

Lazy proof explication is a theorem-proving architecture that allows a combination of Nelson-Oppen-style decision procedures to leverage a SAT solver’s ability to perform propositional reasoning efficiently. The SAT solver finds ways to satisfy a given formula propositionally, while the various decision procedures perform theory reasoning to block propositionally satisfied instances that are not consistent with the theories. Supporting quantifiers in this architecture poses a challenge as quantifier instantiations can dynamically introduce boolean structure in the formula, requiring a tighter interleaving between propositional and theory reasoning.

This paper proposes handling quantifiers by using two SAT solvers, thereby separating the propositional reasoning of the input formula from that of the instantiated formulas. This technique can then reduce the propositional search space, as the paper demonstrates. The technique can use off-the-shelf SAT solvers and requires only that the theories are checkpointable.

This paper addresses the problem of generating symbolic test cases for testing the conformance of a black-box implementation with respect to a specification, in the context of reactive systems. The challenge we consider is the selection of test cases according to a test purpose, which is here a set of scenarios of interest that one wants to observe during test execution. Because of the interactions that occur between the test case and the implementation, test execution can be seen as a game involving two players, in which the test case attempts to satisfy the test purpose.

Efficient solutions to this problem have been proposed in the context of finite-state models, based on the use of fixpoint computations. We extend them in the context of infinite-state symbolic models, by showing how approximate fixpoint computations can be used in a conservative way. The second contribution we provide is the formalization of a quality criterium for test cases, and a result relating the quality of a generated test case to the approximations used in the selection algorithm.

Object-oriented unit tests consist of sequences of method invocations. Behavior of an invocation depends on the method’s arguments and the state of the receiver at the beginning of the invocation. Correspondingly, generating unit tests involves two tasks: generating method sequences that build relevant receiver-object states and generating relevant method arguments. This paper proposes Symstra, a framework that achieves both test generation tasks using symbolic execution of method sequences with symbolic arguments. The paper defines symbolic states of object-oriented programs and novel comparisons of states. Given a set of methods from the class under test and a bound on the length of sequences, Symstra systematically explores the object-state space of the class and prunes this exploration based on the state comparisons. Experimental results show that Symstra generates unit tests that achieve higher branch coverage faster than the existing test-generation techniques based on concrete method arguments.

is a technique to combat the state explosion problem in temporal logic model checking. Its use with symbolic representation has suffered from the prohibitively large BDD for the . One suggested solution is to pre-compute a mapping from states to possibly of symmetry equivalence classes. In this paper, we propose a more efficient method that determines representatives dynamically during fixpoint iterations. Our scheme preserves the uniqueness of representatives. Another alternative to using the orbit relation is . It proved efficient for the special case of full symmetry, provided a conducive program structure. In contrast, our solution applies also to systems with less than full symmetry, and to systems where a translation into counters is not feasible. We support these claims with experimental results.

In the domain of software verification, predicate abstraction has emerged to be a powerful and popular technique for extracting finite-state models from often complex source code. In this paper, we report on the application of three techniques for improving the performance of the predicate abstraction refinement loop. The first technique allows faster computation of the abstraction. Instead of maintaining a global set of predicates, we find predicates relevant to various basic blocks of the program by weakest pre-condition propagation along spurious program traces. The second technique enables faster model checking of the abstraction by reducing the number of state variables in the abstraction. This is done by re-using Boolean variables to represent different predicates in the abstraction. However, some predicates are useful at many program locations and discovering them lazily in various parts of the program leads to a large number of abstraction refinement iterations. The third technique attempts to identify such predicates early in the abstraction refinement loop and handles them separately by introducing dedicated state variables for such predicates. We have incorporated these techniques into NEC’s software verification tool , and present promising experimental results for various case studies using these techniques.

Transformations using retiming and resynthesis operations are the most important and practical (if not the only) techniques used in optimizing synchronous hardware systems. Although these transformations have been studied extensively for over a decade, questions about their and are not answered fully. Resolving these questions may be crucial in developing more effective synthesis and verification algorithms. This paper settles the above two open problems. The optimization potential is resolved through a constructive algorithm which determines if two given finite state machines (FSMs) are transformable to each other via retiming and resynthesis operations. Verifying the equivalence of two FSMs under such transformations, when the history of iterative transformation is unknown, is proved to be PSPACE-complete and hence just as hard as general equivalence checking, contrary to a common belief. As a result, we advocate a conservative design methodology for the optimization of synchronous hardware systems to ameliorate verifiability. Our analysis reveals some properties about initializing FSMs transformed under retiming and resynthesis. On the positive side, established is a lag-independent bound on the length increase of initialization sequences for FSMs under retiming. It allows a simpler incremental construction of initialization sequences compared to prior approaches. On the negative side, we show that there is no analogous transformation-independent bound when resynthesis and retiming are iterated. Fortunately, an algorithm computing the exact length increase is presented.

Communicating Finite States Machines (CFMs) and Message Sequence Graphs (MSC-graphs for short) are two popular specification formalisms for communicating systems. MSC-graphs capture requirements (scenarios), hence they are the starting point of the design process. Implementing an MSC-graph means obtaining an equivalent CFM, since CFMs correspond to distributed message-passing algorithms. Several partial answers for the implementation have been proposed. E.g., local-choice MSC-graphs form a subclass of deadlock-free CFM: Testing equivalence with some local-choice MSC-graph is thus a partial answer to the implementation problem. Using Compositional MSCs, we propose a new algorithm which captures more implementable models than with MSCs. Furthermore, the size of the implementation is reduced by one exponential.

We provide semantics for the powerful scenario-based language of live sequence charts (LSCs). We show how the semantics of live sequence charts can be captured using temporal logic. This is done by studying various subsets of the LSC language and providing an explicit translation into temporal logic. We show how a kernel subset of the LSC language (which omits variables, for example) can be embedded within the temporal logic CTL. For this kernel subset the embedding is a strict inclusion. We show that existential charts can be expressed using the branching temporal logic CTL while universal charts are in the intersection of linear temporal logic and branching temporal logic LTL ∩ CTL. Since our translations are efficient, the work described here may be used in the development of tools for analyzing and executing scenario-based requirements and for verifying systems against such requirements.

Specifications are necessary in order to find software bugs using program verification tools. This paper presents a novel automatic specification mining algorithm that uses information about error handling to learn temporal safety rules. Our algorithm is based on the observation that programs often make mistakes along exceptional control-flow paths, even when they behave correctly on normal execution paths. We show that this focus improves the effectiveness of the miner for discovering specifications beneficial for bug finding.

We present quantitative results comparing our technique to four existing miners. We highlight assumptions made by various miners that are not always born out in practice. Additionally, we apply our algorithm to existing Java programs and analyze its ability to learn specifications that find bugs in those programs. In our experiments, we find filtering candidate specifications to be more important than ranking them. We find 430 bugs in 1 million lines of code. Notably, we find 250 more bugs using per-program specifications learned by our algorithm than with generic specifications that apply to all programs.