I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - Putting Newton into Practice: A Solver for Polynomial Equations over Semirings


M. Schlund, M. Terepeta, and M. Luttenberger. Putting Newton into Practice: A Solver for Polynomial Equations over Semirings. In LPAR 2013, volume 8312 of Lecture Notes in Computer Science, pages 727–734, December 2013.


We present the first implementation of Newton's method for solving systems of equations over -continuous semirings (based on iteDBLP:journals/jacm/EsparzaKL10,DBLP:conflataLuttenbergerS13). For instance, such equation systems arise naturally in the analysis of interprocedural programs or the provenance computation for Datalog. Our implementation provides an attractive alternative for computing their exact least solution in some cases where the ascending chain condition is not met and hence, standard fixed-point iteration needs to be combined with some over-approximation (e.g., widening techniques) to terminate. We present a generic C++ library along with the main algorithms and analyze their complexity. Furthermore, we describe our implementation of the counting semiring based on semilinear sets. Finally, we discuss motivating examples as well as performance benchmarks.

Suggested BibTeX entry:

    author = {M. Schlund and M. Terepeta and M. Luttenberger},
    booktitle = {LPAR 2013},
    month = {December},
    pages = {727--734},
    series = {Lecture Notes in Computer Science},
    title = {Putting {N}ewton into {P}ractice: {A} {S}olver for {P}olynomial {E}quations over {S}emirings},
    volume = {8312},
    year = {2013}

PDF (324 kB)