Numeric Program Analysis Techniques with Applications to Array Analysis and Library Summarization

Abstract

Numeric program analysis is of great importance for the areas of software engineering, software verification, and security: to identify many program errors, such as out-of-bounds array accesses and integer overflows, which constitute the lions share of security vulnerabilities reported by CERT, an analyzer needs to establish numeric properties of program variables. Many important program analyses, such as low-level code analysis, memory-cleanness analysis, and shape analysis, rely in some ways on numeric-program-analysis techniques. However, existing numeric abstractions are complex (numeric abstract domains are typically non-distributive, and form infinite-height lattices); thus, obtaining precise numeric-analysis results is by no means a trivial undertaking. In this thesis, we develop a suite of techniques with the common goal of improving the precision and applicability of numeric program analysis.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2007
Accession Number
AD1004527

Entities

People

  • Denis Gopan

Organizations

  • University of Wisconsin–Madison

Tags

Communities of Interest

  • C4I
  • Cyber
  • Energy and Power Technologies
  • Space

DTIC Thesaurus Topics

  • Algorithms
  • Analyzers
  • Artificial Intelligence
  • Case Studies
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Detectors
  • Engineering
  • Language
  • Linear Programming
  • Materials
  • Measurement
  • Safety Analysis
  • Software Development
  • Space Exploration

Fields of Study

  • Engineering

Readers

  • Computer Programming and Software Development.
  • Software Engineering.