A Static Analysis Tool with Optimizations for Reachability Determination
Sponsor
This research is sponsored in part by NSFC Program (No. 91218302, No. 61527812, 61402248), National Science and Technology Major Project (No. 2016ZX01038101), MIIT IT funds (Research and application of TCN key technologies ) of China, and The National Key Technology R&D Program (No. 2015BAG14B01-02).
Published In
ASE 2017: Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering
ISBN
978-1-5386-2684-9
Document Type
Citation
Publication Date
10-30-2017
Abstract
To reduce the false positives of static analysis, many tools collect path constraints and integrate SMT solvers to filter unreachable execution paths. However, the accumulated calling and computing of SMT solvers are time and resource consuming. This paper presents TsmartLW, an alternate static analysis tool in which we implement a path constraint solving engine to speed up reachability determination. Within the engine, typical types of constraint-patterns are firstly defined based on an empirical study of a large number of code repositories. For each pattern, a constraint solving algorithm is designed and implemented. For each program, the engine predicts the most suitable strategy and then applies the strategy to solve path constraints. The experimental results on some well-known benchmarks and real-world applications show that TsmartLW is faster than some state-of-the-art static analysis tools. For example, it is 1.32x faster than CPAchecker and our engine is 369x faster than SMT solvers in solving path constraints.
Locate the Document
DOI
10.1109/ASE.2017.8115706
Persistent Identifier
https://archives.pdx.edu/ds/psu/30639
Citation Details
Wang, Y., Zhou, M., Jiang, Y., Song, X., Gu, M., & Sun, J. (2017, October). A static analysis tool with optimizations for reachability determination. In Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering (pp. 925-930). IEEE Press.
Description
©2017 IEEE