Abstract
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.
Because essentially all fast iterative numerical methods are forms of Newton’s method, this advance is exciting because it may provide the key to creating faster program-analysis algorithms. However, there is an important difference between the dataflow-analysis and numerical-analysis contexts: when Newton’s method is used in numerical problems, commutativity of multiplication is relied on to rearrange an expression of the form “\(a * Y * b + c * Y * d\)” into “\((a * b + c * d) * Y\).” 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 * Y * b + c * Y * d\)” cannot be rearranged into “\((a * b + c * d) * Y\).” Equations with the former expressions correspond to path problems described by linear context-free languages (LCFLs).
The invited talk that this paper accompanies presented a method that we developed in 2015 for solving the LCFL sub-problems produced during successive rounds of Newton’s method. It uses some algebraic slight-of-hand to turn a class of LCFL path problems into regular-language path problems. This result is surprising because a reasonable sanity check—formal-language theory—suggests that it should be impossible: after all, the LCFL languages are a strict superset of the regular languages.
The talk summarized several concepts and prior results on which that result is based. The method described applies to predicate abstraction, on which most of today’s software model checkers rely, as well as to other abstract domains used in program analysis.
Portions of this work are excerpted from [12].
T. Reps has an ownership interest in GrammaTech, Inc., which has licensed elements of the technology discussed in this publication.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
See [2, Sect. 5.1] for an interprocedural dataflow-analysis method that uses a somewhat similar approach.
- 2.
- 3.
A weight can also be thought of as a Boolean matrix with dimensions \(|A| \times |A|\).
- 4.
For reasons that are immaterial to this discussion, Esparza et al. start the iteration via \({\overrightarrow{\nu }}^{(0)} = {\overrightarrow{f}}({\overrightarrow{\bot }})\), rather than \({\overrightarrow{\nu }}^{(0)} = {\overrightarrow{\bot }}\). Our goal here is to bring out the essential similarities between Eqs. (3) and (4).
References
Ball, T., Rajamani, S.K.: Bebop: a symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000). https://doi.org/10.1007/10722468_7
Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL (2003)
Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Neuhold, E. (ed.) Formal Descriptions of Programming Concepts, IFIP WG 2.2, St. Andrews, Canada, August 1977, pp. 237–277. North-Holland (1978)
Esparza, J., Kiefer, S., Luttenberger, M.: Newtonian program analysis. J. ACM 57(6), 33 (2010)
Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. J. ACM 56(1), 1 (2009)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_10
Hopkins, M., Kozen, D.: Parikh’s theorem in commutative Kleene algebra. In: LICS (1999)
Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Kastens, U., Pfahler, P. (eds.) CC 1992. LNCS, vol. 641, pp. 125–140. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55984-1_13
Lal, A., Reps, T., Balakrishnan, G.: Extended weighted pushdown systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 434–448. Springer, Heidelberg (2005). https://doi.org/10.1007/11513988_44
Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL (2004)
Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL (1995)
Reps, T., Turetsky, E., Prabhu, P.: Newtonian program analysis via tensor product. TOPLAS 39(2), 9 (2017)
Sharir, M., Pnueli, A.: Two Approaches to Interprocedural Data Flow Analysis. In: Program Flow Analysis: Theory and Applications. Prentice-Hall (1981)
Tarjan, R.: Fast algorithms for solving path problems. J. ACM 28(3), 594–614 (1981)
Tarjan, R.: A unified approach to path problems. J. ACM 28(3), 577–593 (1981)
Acknowledgments
This work was supported, in part, by a gift from Rajiv and Ritu Batra; DARPA MUSE award FA8750-14-2-0270 and DARPA STAC award FA8750-15-C-0082; and by the UW-Madison Office of the Vice Chancellor for Research and Graduate Education with funding from the Wisconsin Alumni Research Foundation. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the authors, and do not necessarily reflect the views of the sponsoring agencies.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Reps, T. (2019). Program Analyses Using Newton’s Method (Invited Paper). In: Podelski, A., Taïani, F. (eds) Networked Systems. NETYS 2018. Lecture Notes in Computer Science(), vol 11028. Springer, Cham. https://doi.org/10.1007/978-3-030-05529-5_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-05529-5_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-05528-8
Online ISBN: 978-3-030-05529-5
eBook Packages: Computer ScienceComputer Science (R0)