About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
WHTSU 2012
Workshop paper
Verification of software changes with ExpliSAT
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. © 2012 IEEE.