Verification of software changes with ExpliSAT

Hana Chockler, Sitvanit Ruah

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

1 Citation (Scopus)
16 Downloads (Pure)

Abstract

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 traverse through the changed nodes in the graph. We implemented this idea on top of the concolic model checker ExpliSAT and the experimental results on real programs show a significant improvement in performance compared to re-verification of the whole program, when the change involves a small fraction of paths on the control flow graph.
Original languageEnglish
Title of host publicationInternational Workshop on Hot Topics in Software Upgrades (HotSWUp)
PublisherIEEE Computer Society
Pages31-35
Number of pages5
Publication statusPublished - 3 Jun 2012

Fingerprint

Dive into the research topics of 'Verification of software changes with ExpliSAT'. Together they form a unique fingerprint.

Cite this