Lecture Notes in Computer Science, 1998, Volume 1503/1998, 200-214, DOI: 10.1007/3-540-49727-7_12

Refining Static Analyses by Trace-Based Partitioning Using Control Flow

Maria Handjieva and Stanislav Tzolovski

View Related Documents

Abstract

This paper presents a systematic method of building a more precise static analysis from a given one. The key idea is to lift an abstract domain to the finite sets of its labeled abstract properties. The labels are designed to gather information about the history of control flow and to obtain a finite partitioning of the program execution traces. The abstract operations of the lifted domain are derived from those of the original one. This is a particular instance of the reduced cardinal power introduced by P. and R. Cousot, where the base is the set of labels approximating the control history and the exponent is an abstract domain. The method is applied to the domain of convex polyhedra and to the domain of linear congruences.

Key words  abstract interpretation - reduced cardinal power - trace semantics

Fulltext Preview

Image of the first page of the fulltext document