Enhancing Symbolic Execution to Test the Compatibility of Re-engineered Industrial Software

After a legacy system is re-engineered, it is important to perform compatibility testing so as to identify the difference and reduce the introduced bugs. We can first apply symbolic execution to obtain an exhaustive set of test cases, then use them to check the compatibility of the old system and the new old. However, the path explosion problem of symbolic execution makes it difficult to work on realistic non-trivial applications. We show in this paper how to enhance symbolic execution, e.g. with extra constraints, path cutting, variable grouping, and test case selection, to successfully test the compatibility of an SMTP library (used in embedded systems) with around 20K lines of code. Our experience indicates that these enhancements are essential to apply symbolic execution on realistic industrial applications.