Write a Blog >>
Fri 22 Jan 2016 10:30 - 10:55 at Grand Bay North - Track 1: Program Design and Analysis Chair(s): Manu Sridharan

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 “cX + Xd” 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: “cX + Xd” 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.

Fri 22 Jan

POPL-2016-papers
10:30 - 12:10: Research Papers - Track 1: Program Design and Analysis at Grand Bay North
Chair(s): Manu SridharanSamsung Research America
POPL-2016-papers10:30 - 10:55
Talk
Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc., Emma TuretskyCS Dept., Univ. of Wisconsin-Madison, Prathmesh PrabhuGoogle
Media Attached
POPL-2016-papers10:55 - 11:20
Talk
Rongxin WuDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiao XiaoThe Hong Kong University of Science and Technology, Shing-Chi CheungDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Hongyu ZhangMicrosoft Research, Charles ZhangHKUST
Media Attached
POPL-2016-papers11:20 - 11:45
Talk
Thomas GilrayUniversity of Utah, Steven Lyde, Michael D. AdamsUniversity of Utah, Matthew MightUniversity of Utah, USA, David Van HornUniversity of Maryland, College Park
Pre-print Media Attached
POPL-2016-papers11:45 - 12:10
Talk
Matthew FlattUniversity of Utah
Pre-print Media Attached