Abstract
In this chapter we describe an algorithm for efficient formal verification of changes in software built on top of a model checking procedure that traverses the control flow graph explicitly while representing the data symbolically. The main idea of our algorithm is to guide the control flow graph exploration first to the paths that go through the changed nodes in the graph. This idea can, in fact, be implemented on top of any validation tool that traverses the control flow graph explicitly, as we explain in more detail below. In our experiments, we implemented this algorithm on top of the concolic model checker ExpliSAT, developed at IBM, and the experimental results on real programs showed a significant improvement in performance compared to re-verification of the whole program. Unsurprisingly, the speedup is especially significant when the change involves a small fraction of paths in the control flow graph—a situation typical of a small upgrade.
| Original language | English |
|---|---|
| Title of host publication | Validation of Evolving Software |
| Publisher | Springer International Publishing Switzerland |
| Pages | 25-36 |
| Number of pages | 12 |
| ISBN (Print) | 9783319106236, 9783319106229 |
| DOIs | |
| Publication status | Published - 1 Jan 2015 |