Second-Order Abstract Interpretation via Kleene Algebra

Abstract

Most standard approaches to the static analysis of programs, such as the popular worklist method, are first-order methods that inductively annotate program points with abstract values. In this paper we introduce a second-order approach based on Kleene algebra. In this approach, the primary objects of interest are not the abstract data values, but the transfer functions that manipulate them. These elements form a left-handed Kleene algebra. The dataflow labeling is not achieved by inductively labeling the program with abstract values, but rather by computing the star (Kleene closure)of a matrix of transfer functions. In this paper we introduce the method and prove soundness and completeness with respect to the standard worklist algorithm.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 01, 2004
Accession Number
AD1000906

Entities

People

  • Dexter Kozen
  • Lucja Kot

Organizations

  • Cornell University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Boolean Algebra
  • Computations
  • Computer Science
  • Computers
  • Device Drivers
  • Finite Alphabet
  • Inequalities
  • Instructions
  • Language
  • Monotone Functions
  • New York
  • Object Code
  • Standards
  • Transfer Functions

Readers

  • Approximation Theory.
  • Computational Linguistics
  • Nanofabrication and Microfabrication.