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
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10: Track 1: Program Design and AnalysisResearch Papers at Grand Bay North
Chair(s): Manu SridharanSamsung Research America
10:30 - 10:55
Talk
Research Papers
Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc., Emma TuretskyCS Dept., Univ. of Wisconsin-Madison, Prathmesh PrabhuGoogle
Media Attached
10:55 - 11:20
Talk
Research Papers
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
11:20 - 11:45
Talk
Research Papers
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
11:45 - 12:10
Talk
Research Papers
Matthew FlattUniversity of Utah
Pre-print Media Attached