dc.contributor.author Reps, Thomas dc.contributor.author Turetsky, Emma dc.contributor.author Prabhu, Prathmesh dc.date.accessioned 2016-02-15T19:19:34Z dc.date.available 2016-02-15T19:19:34Z dc.date.issued 2016-02-10 dc.identifier.citation TR1825 en dc.identifier.uri http://digital.library.wisc.edu/1793/74047 dc.description.abstract 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. en 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 ``c*X + X*d'' into ``(c+d) * X.'' Such equations 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: ``c*X + X*d'' cannot be rearranged into ``(c+d) * X.'' Such equations 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. dc.subject tensor product en dc.subject regular expression en dc.subject semiring en dc.subject interprocedural program analysis en dc.subject polynomial fixed-point equation en dc.subject Newton's method en dc.title Newtonian Program Analysis via Tensor Product en dc.type Technical Report en
﻿

### This item appears in the following Collection(s)

• CS Technical Reports
Technical Reports Archive for the Department of Computer Sciences at the University of Wisconsin-Madison