Catálogo de publicaciones - libros

Software analysis and verification require abstraction of the program under consideration. As a result, many reported errors may in fact be false alarms. The Orion static analyzer reduces the ratio of false alarms by performing a state space exploration at two levels of precision. At the first level, a conservative analysis is performed. This detects all errors of a certain kind, but with a potentially high number of superfluous warnings. At the second level, each potential-error trace that is produced at the first level, is subjected to a feasibility analysis using symbolic reasoning - typically by invoking third-party decision procedures. If a trace cannot be shown to be infeasible, it is reported. Orion’s precision can be tuned by varying the resources spent in the second level.

With the increase in the complexity of computer systems, it becomes even more important to develop formal methods for ensuring their quality. Various techniques for automated and semi-automated analysis and verification have been proposed. In particular, model-checking has become a very practical technique due to its push-button character. The basic principle behind model-checking is to build a model of the system under consideration together with a formal description of the verified property in a suitable temporal logic. The model-checking algorithm is a decision procedure which in addition to the yes/no answer returns a trace of a faulty behaviour in case the checked property is not satisfied by the model. One of the additional advantages of this approach is that verification can be performed against partial specifications, by considering only a subset of all specification requirements. This allows for increased efficiency by checking correctness with respect to only the most relevant requirements that should be fulfilled.

Counterexample-guided abstraction refinement (CEGAR) is a key technique for the verification of computer programs. Grumberg et al. developed a CEGAR-based algorithm for the modal -calculus. There, every abstract state is split in a refinement step. In this paper, the work of Grumberg et al. is generalized by presenting a new CEGAR-based algorithm for the -calculus. It is based on a more expressive abstract model and applies refinement only locally (at a single abstract state), i.e., the technique for safety properties is adapted to the -calculus. Furthermore, it separates refinement determination from the (3-valued based) model checking. Three different heuristics for refinement determination are presented and illustrated.

We propose an algorithm to compute a counterexample of minimal size to some property in a finite state program, using the same space constraints than SPIN. This algorithm uses nested breadth-first searches guided by a priority queue. It works in time and is linear in memory.

Computational resources are increasing rapidly with the explosion of multi-core processors readily available from major vendors. Model checking needs to harness these resources to help make it more effective in practical verification. Directed model checking uses heuristics in a guided search to rank states in order of interest. Randomizing guided search makes it possible to harness computation nodes by running independent searches in parallel in a effort to discover counter-examples to correctness. Initial attempts at adding randomization to guided search have achieved very limited success. In this work, we present a new low-cost randomized guided search technique that shuffles states in the priority queue with equivalent heuristic ties. We show in an empirical study that randomized guided search, overall, decreases the number of states generated before error discovery when compared to a guided search using the same heuristic. To further evaluate the performance gains of randomized guided search using a particular heuristic, we compare it with randomized depth-first search. Randomized depth-first search shuffles transitions and generally improves error discovery over the default transition order implemented by the model checker. In the context of evaluating randomized guided search, a randomized depth-first search provides a lower bound for establishing performance gains in directed model checking. In the empirical study, we show that with the correct heuristic, randomized guided search outperforms randomized depth-first search both in effectively finding counter-examples and generating shorter counter-examples.

Runtime (dynamic) model checking is a promising verification methodology for real-world threaded software because of its many features, the prominent ones being: (i) it avoids the need to extract a model and instead runs the actual code, and (ii) the precision of information available at run-time allows techniques such as dynamic partial order reduction (DPOR) [1] to dramatically cut down the number of interleavings examined. Unfortunately, DPOR does not have many implementations for real thread libraries such as POSIX Pthreads, and suffers from high computational overheads due to a stateless search that requires re-executions. In our previous work [2], we designed a runtime model checker, , that overcomes the first of these drawbacks. has been shown capable of detecting data races, deadlocks and other incorrect API usages in real-world PThreads C programs. In this paper, we describe a distributed version of , which implements an extended DPOR algorithm. Our two key contributions are: (i) a practical algorithm for distributed dynamic partial order reduction; (ii) the innovations that helped distributed attain nearly linear (with respect to the number of CPUs) speedup on realistic examples.

The ignoring problem refers to the fact that some actions may be infinitely postponed by a state space search algorithm that makes use of partial order reduction (POR). The prevention of this phenomenon is mandatory if one wants to verify more elaborate properties than the deadlock freeness, e.g., safety or liveness properties. We present in this work some solutions to this problem. In order to assess the quality of our propositions, we included them in our model checker Helena. We report the result of some experiments which show that our algorithms yield better reductions than state of the art algorithms like those implemented in the Spin tool.

Verifying concurrent programs is challenging since the number of thread interleavings that need to be explored can be huge even for moderate programs. We present a that reduces the amount of non-determinism in concurrent programs by delaying unnecessary context switches. Using this semantics, we construct a novel dynamic partial-order reduction algorithm. We have implemented our algorithm and evaluate it on a small set of benchmarks. Our preliminary experimental results show a significant potential saving in the number of explored states and transitions.

State explosion in model checking continues to be the primary obstacle to widespread use of software model checking. The large input ranges of variables used in software is the main cause of state explosion. As software grows in size and complexity, the problem only becomes worse. As such, model checking research into data abstraction as a way of mitigating state explosion has become more and more important. Data abstractions aim to reduce the effect of large input ranges. This work focuses on a static program analysis technique called dead variable analysis. The goal of dead variable analysis is to discover variable assignments that are not used. When applied to model checking, this allows us to ignore the entire input range of dead variables and thus reduce the size of the explored state space.

Prior research into dead variable analysis for model checking does not make full use of dynamic run-time information that is present during model checking. We present an algorithm for intraprocedural dead variable analysis that uses dynamic run-time information to find more dead variables on-the-fly and further reduce the size of the explored state space. We introduce a definition for the maximal state space reduction possible through an on-the-fly dead variable analysis and then show that our algorithm produces a maximal reduction in the absence of non-determinism.