zbMATH — the first resource for mathematics

Program analysis using symbolic ranges. (English) Zbl 1211.68101
Nielson, Hanne Riis (ed.) et al., Static analysis. 14th international symposium, SAS 2007, Kongens Lyngby, Denmark, August 22–24, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-74060-5/pbk). Lecture Notes in Computer Science 4634, 366-383 (2007).
Summary: Interval analysis seeks static lower and upper bounds on the values of program variables. These bounds are useful, especially for inferring invariants to prove buffer overflow checks. In practice, however, intervals by themselves are often inadequate as invariants due to the lack of relational information among program variables.
In this paper, we present a technique for deriving symbolic bounds on variable values. We study a restricted class of polyhedra whose constraints are stratified with respect to some variable ordering provided by the user, or chosen heuristically. We define a notion of normalization for such constraints and demonstrate polynomial time domain operations on the resulting domain of symbolic range constraints. The abstract domain is intended to complement widely used domains such as intervals and octagons for use in buffer overflow analysis. Finally, we study the impact of our analysis on commercial software using an overflow analyzer for the C language.
For the entire collection see [Zbl 1123.68008].

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
CSSV; Octagon; PPL
Full Text: DOI