Lightweight static analysis check of upgrades in c/c++ software

Hana Chockler*, Sitvanit Ruah

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review


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 languageEnglish
Title of host publicationValidation of Evolving Software
PublisherSpringer International Publishing Switzerland
Number of pages12
ISBN (Print)9783319106236, 9783319106229
Publication statusPublished - 1 Jan 2015


Dive into the research topics of 'Lightweight static analysis check of upgrades in c/c++ software'. Together they form a unique fingerprint.

Cite this