Newtonian Program Analysis via Tensor Product
Thomas Reps†,‡, Emma Turetsky‡, and Prathmesh Prabhu♦
Recently, Esparza et al. generalized Newton's method—a
numerical-analysis algorithm for finding roots of real-valued
functions—to a method for finding fixed-points of systems of
equations over semirings.
Their method provides a new way to solve interprocedural
dataflow-analysis problems.
As in its real-valued counterpart, each iteration of their
method solves a simpler ``linearized'' problem.
One of the reasons this advance is exciting is that
some numerical analysts have claimed that ```all' effective and fast
iterative [numerical] methods are forms (perhaps very disguised) of Newton's method.''
However, there is an important difference between the
dataflow-analysis and numerical-analysis contexts:
when Newton's method is used on numerical-analysis problems,
multiplicative commutativity is relied on to rearrange expressions of
the form ``a*X*b + c*X*d'' into ``(a*b + c*d) * X.''
Equations with such expressions correspond to path problems described
by regular languages.
In contrast, when Newton's method is used for interprocedural dataflow
analysis, the ``multiplication'' operation involves function
composition, and hence is non-commutative:
``a*X*b + c*X*d'' cannot be rearranged into ``(a*b + c*d) * X.''
Equations with such expressions correspond to path problems described
by linear context-free languages (LCFLs).
In this paper, we present an improved technique for solving the LCFL
sub-problems produced during successive rounds of Newton's method.
Our method applies to predicate abstraction, on which most of
today's software model checkers rely.
(Click here to access the paper:
PDF.)
†University of Wisconsin; Madison, WI
‡GrammaTech, Inc.; Ithaca, NY
♦Google, Inc.; Mountain View, CA