**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.)