Program analysis using symbolic ranges

Sriram Sankaranarayanan, Franjo Ivančić, Aarti Gupta

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

24 Scopus citations

Abstract

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
Pages366-383
Number of pages18
ISBN (Print)9783540740605
DOIs
StatePublished - Jan 1 2007
Externally publishedYes
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

Other

Other14th International Static Analysis Symposium, SAS 2007
CountryDenmark
CityKongens Lyngby
Period8/22/078/24/07

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

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

  • Cite this

    Sankaranarayanan, S., Ivančić, F., & Gupta, A. (2007). Program analysis using symbolic ranges. In Static Analysis - 14th International Symposium, SAS 2007, Proceedings (pp. 366-383). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4634 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-540-74061-2_23