Possible Value Analysis based on Symbolic Lattice

TL;DR

This paper introduces a novel static program analysis called program behavior analysis that computes possible symbolic expressions for variables at each program point, utilizing a new lattice, transfer function, and widening operator, extended interprocedurally.

Contribution

The paper presents a new static analysis framework with a specialized lattice, transfer function, and widening operator, extended to interprocedural analysis, advancing symbolic expression analysis.

Findings

Developed a new lattice for symbolic analysis

Designed transfer functions and widening operators

Extended analysis to interprocedural contexts

Abstract

We propose a new static program analysis called program behavior analysis. The analysis aims to calculate possible symbolic expressions for every variable at each program point. We design a new lattice, transfer function, and widening operator to accommodate the analysis. Furthermore, we extend the analysis to interprocedural.