Newtonian Program Analysis via Tensor Product
| Autor: | Emma Turetsky, Prathmesh Prabhu, Thomas Reps |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Computer science
0102 computer and information sciences 02 engineering and technology System of linear equations 01 natural sciences semiring Semiring symbols.namesake Predicate abstraction interprocedural program analysis Regular language 0103 physical sciences Newtonian fluid 0202 electrical engineering electronic engineering information engineering Newton's method Commutative property 010302 applied physics tensor product 020207 software engineering Computer Graphics and Computer-Aided Design Algebra Tensor product Newton fractal polynomial fixed-point equation 010201 computation theory & mathematics symbols regular expression Multiplication Function composition Algorithm Software |
| Zdroj: | POPL |
| ISSN: | 2381-3652 |
| Popis: | 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 in numerical-analysis problems, commutativity of multiplication is relied on to rearrange an expression 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 article, 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|