Modular demand-driven analysis of semantic difference for program versions

Conference item

In this work we present a modular and demand-driven analysis of the semantic difference between program versions. Our analysis characterizes initial states for which final states in the pro- gram versions are different. It also characterizes states for which the final states are identical. Such characterizations are useful for regression veri- fication, for revealing security vulnerabilities, and for identifying changes in the program's functionality. Syntactic changes in program versions are often small and local and may apply to procedures that are deep in the procedure call graph. Our approach analyses only those parts of the programs that are affected by the changes. Moreover, the analysis is modular, applied to a single pair of procedures at a time. Called procedures are not inlined. Rather, their previously computed summaries and difference summary are used. For efficiency, procedure summaries and difference summaries can be abstracted and may be refined on-demand. We implemented our method and applied it to finding semantic difference between program versions. We compared it to well established tools and observed speedups of one order of magnitude and more. Further, in many cases our tool could prove equivalence or find difierences, while the others failed to do so.

Authors: Trostanetski, A; Grumberg, O; Kroening, D

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Springer Verlag
• Host title: 24th International Static Analysis Symposium, August 30th - September 1st, 2017, New York City, NY, USA
• Journal: Static analysis symposium
• Pages: 405-427
• Publication date: 2017-08-19
• Acceptance date: 2017-06-12
• DOI: 10.1007/978-3-319-66706-5_20
• ISBN: 9783319667065