Program analysis using symbolic ranges

Sriram Sankaranarayanan, Franjo Ivančić, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

29 Scopus citations


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.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 14th International Symposium, SAS 2007, Proceedings
PublisherSpringer Verlag
Number of pages18
ISBN (Print)9783540740605
StatePublished - 2007
Event14th International Static Analysis Symposium, SAS 2007 - Kongens Lyngby, Denmark
Duration: Aug 22 2007Aug 24 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4634 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other14th International Static Analysis Symposium, SAS 2007
CityKongens Lyngby

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Program analysis using symbolic ranges'. Together they form a unique fingerprint.

Cite this