×

Static analysis in disjunctive numerical domains. (English) Zbl 1225.68077

Yi, Kwangkeun (ed.), Static analysis. 13th international symposium, SAS 2006, Seoul, Korea, August 29–31, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-37756-6/pbk). Lecture Notes in Computer Science 4134, 3-17 (2006).
Summary: The convexity of numerical domains such as polyhedra, octagons, intervals and linear equalities enables tractable analysis of software for buffer overflows, null pointer dereferences and floating point errors. However, convexity also causes the analysis to fail in many common cases. Powerset extensions can remedy this shortcoming by considering disjunctions of predicates. Unfortunately, analysis using powerset domains can be exponentially more expensive as compared to analysis on the base domain. In this paper, we prove structural properties of fixed points computed in commonly used powerset extensions. We show that a fixed point computed on a powerset extension is also a fixed point in the base domain computed on an “elaboration” of the program’s CFG structure. Using this insight, we build analysis algorithms that approach path sensitive static analysis algorithms by performing the fixed point computation on the base domain while discovering an “elaboration” on the fly. Using restrictions on the nature of the elaborations, we design algorithms that scale polynomially in terms of the number of disjuncts. We have implemented a light-weight static analyzer for C programs with encouraging initial results.
For the entire collection see [Zbl 1120.68011].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
65Y99 Computer aspects of numerical algorithms
68W40 Analysis of algorithms

Software:

PPL; ASTREE; CSSV
PDF BibTeX XML Cite
Full Text: DOI Link