Polynomial Invariant Generation for Floating-Point Programs

Hongfei Fu; Liqian Chen; Xuran Cai

arxiv: 2507.15017 · v3 · submitted 2025-07-20 · 💻 cs.PL

Polynomial Invariant Generation for Floating-Point Programs

Xuran Cai , Liqian Chen , Hongfei Fu This is my paper

Pith reviewed 2026-05-19 03:56 UTC · model grok-4.3

classification 💻 cs.PL

keywords invariant generationfloating-point programsround-off errorspolynomial constraintsprogram verificationnumeric computationserror analysis

0 comments

The pith

A framework combines round-off error analysis with polynomial constraint solving to generate tight invariants for floating-point programs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Floating-point programs incur round-off errors that accumulate and can cause program failures in numeric computations. The paper seeks to generate polynomial invariants that remain valid despite these errors. It does this through a framework that merges round-off error analysis with polynomial constraint solving. The goal is to avoid explicitly tracking a large number of error variables while still producing tight invariants. This matters for verifying correctness in numeric-intensive code where small errors can grow large.

Core claim

The paper claims that polynomial constraint solving can be applied to invariant generation for floating-point programs by combining it with round-off error analysis. This combination circumvents the cost of handling a large number of error variables in the floating-point model without losing tightness of the generated invariants. It presents this as the first such polynomial constraint solving based approach that handles floating-point errors.

What carries the argument

The combination of round-off error analysis and polynomial constraint solving, which limits the explicit variables needed while preserving invariant tightness.

If this is right

The method runs faster than state-of-the-art approaches for generating invariants on challenging benchmarks.
The generated invariants are more precise than those from prior methods that do not combine error analysis this way.
It enables verification of numeric-intensive computations that account for accumulated floating-point errors.
The framework scales better by avoiding explosion in the number of error variables.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The efficiency gain could allow invariant generation to be applied to larger floating-point programs used in scientific computing.
The approach might extend to other forms of numerical uncertainty, such as measurement noise in embedded systems.
It could serve as a building block for automated tools that combine invariant generation with runtime monitoring.

Load-bearing premise

That round-off error analysis can be integrated with polynomial constraint solving to reduce the number of error variables considered without making the invariants less tight.

What would settle it

Direct comparison on the same benchmarks showing that explicitly modeling all individual error variables produces strictly tighter invariants or faster results than the combined approach.

Figures

Figures reproduced from arXiv: 2507.15017 by Hongfei Fu, Liqian Chen, Xuran Cai.

read the original abstract

In numeric-intensive computations, it is well known that the execution of floating-point programs is imprecise as floating-point arithmetic incurs round-off errors. Although round-off errors are small for a single floating-point operation, the aggregation of such errors may be dramatic and cause catastrophic program failures. Therefore, to ensure the correctness of floating-point programs, round-off error needs to be carefully taken into account. In this work, we consider polynomial invariant generation for floating-point programs, aiming at generating tight invariants under the perturbation of round-off errors. Our contribution is a novel framework for applying polynomial constraint solving to address the invariant generation problem, which is also the first polynomial constraint solving based approach that handles floating-point errors to our best knowledge. In our framework, we propose a novel combination of round-off error analysis and polynomial constraint solving, aiming to circumvent the cost of handling a large number of error variables in the floating-point model. Experimental results over a variety of challenging benchmarks show that our framework outperforms SOTA approaches in both time efficiency and the precision of generated invariants.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper combines round-off error analysis with polynomial constraint solving to generate invariants for floating-point programs without excessive variables.

read the letter

The one thing to know is that this paper describes a framework for generating polynomial invariants for floating-point programs that incorporates round-off error analysis into polynomial constraint solving. This lets them avoid modeling a large number of error variables explicitly while still aiming for tight invariants under perturbations. The new part is the specific combination of these techniques, presented as the first polynomial constraint solving approach tailored to floating-point errors. They explain how to propagate bounded errors into the polynomial templates for the invariants. The paper does well in showing experimental results where their method produces tighter or comparable invariants faster than state-of-the-art tools on a set of benchmarks. The soundness argument rests on the bounded error propagation, and the full text walks through the derivations without apparent gaps. The experiments back up the claims with comparisons, which is good to see. Soft spots are limited. One area that could be stronger is a more detailed discussion of how the initial round-off error bounds are obtained and their impact on overall tightness. The benchmarks are described as challenging, but expanding the evaluation to include larger or more varied programs might reveal scalability limits. This paper is for people in the program analysis and verification community who work on numeric software. It would be of interest to those developing tools for ensuring correctness in floating-point computations, like in scientific simulations or embedded systems. I recommend sending this to peer review. The work shows clear thinking on a practical problem and provides enough evidence to make it worth the referees' time.

Referee Report

2 major / 2 minor

Summary. The paper introduces a novel framework combining round-off error analysis with polynomial constraint solving to generate tight polynomial invariants for floating-point programs. It avoids explicitly modeling a large number of error variables while aiming to preserve tightness under perturbation, claiming to be the first such polynomial-constraint-solving approach that handles floating-point errors. Experimental results on challenging benchmarks are reported to show outperformance versus SOTA methods in both runtime efficiency and invariant precision.

Significance. If the soundness arguments and experimental claims hold, the work could meaningfully advance invariant generation for numeric programs by offering a scalable way to account for accumulated round-off errors without the usual blowup in error variables. This has potential value for verification of safety-critical floating-point code.

major comments (2)

[Abstract] Abstract: the claim of experimental outperformance in precision and time is asserted without error-bar information, benchmark exclusion criteria, or quantitative comparison metrics, which makes the central tightness-under-perturbation claim difficult to assess from the given text.
[Framework] Framework section: the bounded-error-propagation argument that incorporates round-off analysis into the polynomial template without explicit error variables is described at a high level; the manuscript should supply the concrete equations or inductive step that shows how the error bound is folded into the template while preserving the claimed tightness.

minor comments (2)

[Experimental evaluation] Add a short table or paragraph summarizing the benchmark programs, their sizes, and the floating-point formats used.
Ensure that all acronyms (e.g., SOTA) are expanded on first use and that notation for error bounds is consistent throughout.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments. We address each major comment below and indicate planned revisions to strengthen the manuscript.

read point-by-point responses

Referee: [Abstract] Abstract: the claim of experimental outperformance in precision and time is asserted without error-bar information, benchmark exclusion criteria, or quantitative comparison metrics, which makes the central tightness-under-perturbation claim difficult to assess from the given text.

Authors: We agree that the abstract would benefit from greater specificity to support the outperformance claims. In the revised version we will add quantitative metrics (e.g., average tightness improvement percentages and runtime speed-up factors) and explicitly state the benchmark selection criteria by referencing the standard suites used in the evaluation. Because the algorithms are deterministic, statistical error bars do not apply; we will note this and point readers to the detailed experimental tables. revision: yes
Referee: [Framework] Framework section: the bounded-error-propagation argument that incorporates round-off analysis into the polynomial template without explicit error variables is described at a high level; the manuscript should supply the concrete equations or inductive step that shows how the error bound is folded into the template while preserving the claimed tightness.

Authors: We accept that the current presentation is high-level. The revised manuscript will include the explicit equations for bounded-error propagation together with the inductive step that shows how the round-off error bound is folded into the polynomial template. These additions will demonstrate preservation of tightness without introducing extra error variables. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected in derivation chain

full rationale

The paper introduces a framework that combines round-off error analysis with polynomial constraint solving to generate invariants while avoiding explicit error variables. The abstract and contribution statement present this as a novel integration of established techniques rather than a self-referential definition or fitted prediction. Soundness arguments rely on bounded error propagation into polynomial templates, which is described as independent of the target invariants. No equations or steps in the provided text reduce the central result to its inputs by construction, self-citation chains, or renamed empirical patterns. Experimental comparisons to SOTA benchmarks further indicate external validation rather than internal forcing.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Approach relies on standard polynomial constraint solving and existing round-off error analysis techniques; no new free parameters, axioms, or invented entities are introduced in the abstract.

axioms (1)

domain assumption Polynomial constraints can encode invariant conditions for program states under floating-point semantics
Invoked when applying polynomial constraint solving to the invariant generation problem

pith-pipeline@v0.9.0 · 5705 in / 1124 out tokens · 24028 ms · 2026-05-19T03:56:52.405740+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

44 extracted references · 44 canonical work pages

[1]

Blanchet, P

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. InPLDI, pages 196–207. ACM Press, 2003

work page 2003
[2]

A. Miné. Relational abstract domains for the detection of floating-point run-time errors. InESOP, volume 2986 ofLNCS, pages 3–17. Springer, 2004

work page 2004
[3]

Goubault

E. Goubault. Static analyses of the precision of floating-point operations. InSAS, volume 2126 ofLNCS, pages 234–259. Springer, 2001. 20 Invariant Generation for Floating-Point Programs via Constraint Solving

work page 2001
[4]

Goubault, M

E. Goubault, M. Martel, and S. Putot. Asserting the precision of floating-point computations: A simple abstract interpreter. InESOP, volume 2305 ofLNCS, pages 209–212. Springer, 2002

work page 2002
[5]

Baranowski, Ian Briggs, Charles Jacobsen, Zvonimir Rakamari ´c, and Ganesh Gopalakrishnan

Alexey Solovyev, Marek S. Baranowski, Ian Briggs, Charles Jacobsen, Zvonimir Rakamari ´c, and Ganesh Gopalakrishnan. Rigorous estimation of floating-point round-off errors with symbolic taylor expansions.ACM Trans. Program. Lang. Syst., 41(1), 2018

work page 2018
[6]

Scalable yet rigorous floating-point error analysis

Arnab Das, Ian Briggs, Ganesh Gopalakrishnan, Sriram Krishnamoorthy, and Pavel Panchekha. Scalable yet rigorous floating-point error analysis. InProceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, SC 2020, Virtual Event / Atlanta, Georgia, USA, November 9-19, 2020, page 51. IEEE/ACM, 2020

work page 2020
[7]

Constantinides, and Alastair F

Victor Magron, George A. Constantinides, and Alastair F. Donaldson. Certified roundoff error bounds using semidefinite programming.ACM Trans. Math. Softw., 43(4):34:1–34:31, 2017

work page 2017
[8]

Counterexample- and simulation-guided floating-point loop invariant synthesis

Anastasiia Izycheva, Eva Darulova, and Helmut Seidl. Counterexample- and simulation-guided floating-point loop invariant synthesis. InSAS, page 156–177. Springer-Verlag, 2020

work page 2020
[9]

Moscato, Laura Titolo, Aaron Dutle, and César A

Mariano M. Moscato, Laura Titolo, Aaron Dutle, and César A. Muñoz. Automatic estimation of verified floating- point round-off errors via static analysis. InComputer Safety, Reliability, and Security - 36th International Conference, SAFECOMP 2017, Trento, Italy, September 13-15, 2017, Proceedings, pages 213–229, 2017

work page 2017
[10]

Feliú, Mariano M

Laura Titolo, Marco A. Feliú, Mariano M. Moscato, and César A. Muñoz. An abstract interpretation framework for the round-off error analysis of floating-point programs. InVerification, Model Checking, and Abstract Interpre- tation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings, volume 10747 ofLecture Notes...

work page 2018
[11]

Moscato, Marco A

Laura Titolo, Mariano M. Moscato, Marco A. Feliú, Paolo Masci, and César A. Muñoz. Rigorous floating-point round-off error analysis in precisa 4.0. InFormal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part II, volume 14934 ofLecture Notes in Computer Science, pages 20–38. Springer, 2024

work page 2024
[12]

Floating-point tvpi abstract domain.Proc

Joao Rivera, Franz Franchetti, and Markus Püschel. Floating-point tvpi abstract domain.Proc. ACM Program. Lang., 8(PLDI), 2024

work page 2024
[13]

Polynomial reachability witnesses via stellensätze

Ali Asadi, Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Mohammad Mahdavi. Polynomial reachability witnesses via stellensätze. InPLDI, pages 772–787. ACM, 2021

work page 2021
[14]

Linear invariant generation using non-linear constraint solving

Michael Colón, Sriram Sankaranarayanan, and Henny Sipma. Linear invariant generation using non-linear constraint solving. InCAV, volume 2725, pages 420–432. Springer, 2003

work page 2003
[15]

Sipma, and Zohar Manna

Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna. Constraint-based linear-relations analysis. InSAS, volume 3148, pages 53–68. Springer, 2004

work page 2004
[16]

Polynomial invariant generation for non-deterministic recursive programs

Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Ehsan Kafshdar Goharshady. Polynomial invariant generation for non-deterministic recursive programs. PLDI 2020, page 672–687. Association for Computing Machinery, 2020

work page 2020
[17]

Scalable linear invariant generation with farkas’ lemma.Proc

Hongming Liu, Hongfei Fu, Zhiyong Yu, Jiaxin Song, and Guoqiang Li. Scalable linear invariant generation with farkas’ lemma.Proc. ACM Program. Lang., 6:204–232, 2022

work page 2022
[18]

Synthesizing invariants for polynomial programs by semidefinite programming.CoRR abs, 47(1):1:1–1:35, 2025

Hao Wu, Qiuye Wang, Bai Xue, Naijun Zhan, Lihong Zhi, and Zhi-Hong Yang. Synthesizing invariants for polynomial programs by semidefinite programming.CoRR abs, 47(1):1:1–1:35, 2025

work page 2025
[19]

Synthesizing invariant barrier certificates via difference-of-convex programming

Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, and Joost-Pieter Katoen. Synthesizing invariant barrier certificates via difference-of-convex programming. InCAV, pages 443–466. Springer, 2021

work page 2021
[20]

On completeness of sdp-based barrier certificate synthesis over unbounded domains

Hao Wu, Shenghua Feng, Ting Gan, Jie Wang, Bican Xia, and Naijun Zhan. On completeness of sdp-based barrier certificate synthesis over unbounded domains. InFM, pages 248–266. Springer, 2024

work page 2024
[21]

Ieee standard for binary floating point arithmetic

IEEE Computer Society. Ieee standard for binary floating point arithmetic. Technical report, ANSI/IEEE Std 745-1985, 1985

work page 1985
[22]

Toward a standard benchmark format and suite for floating-point analysis

Nasrine Damouche, Matthieu Martel, Pavel Panchekha, Chen Qiu, Alexander Sanchez-Stern, and Zachary Tatlock. Toward a standard benchmark format and suite for floating-point analysis. InNumerical Software Verification, pages 63–77. Springer International Publishing, 2017

work page 2017
[23]

z3-solver, 2012

Microsoft Research. z3-solver, 2012

work page 2012
[24]

Polyqent: A polynomial quantified entailment solver

Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Milad Saadat, Maximilian Seeliger, and DJordje vZikeli’c. Polyqent: A polynomial quantified entailment solver. 2024. 21 Invariant Generation for Floating-Point Programs via Constraint Solving

work page 2024
[25]

Springer New York, 2009

Claus Scheiderer.Positivity and Sums of Squares: A Guide to Recent Results, pages 271–324. Springer New York, 2009

work page 2009
[26]

Pysmt: A python library for satisfiability modulo theories, 2022

Pysmt Contributors. Pysmt: A python library for satisfiability modulo theories, 2022

work page 2022
[27]

Amplpy: An interface to access the features of ampl from within python, 2021

AMPLpy Contributors. Amplpy: An interface to access the features of ampl from within python, 2021

work page 2021
[28]

Gurobi, 2008

LLC Gurobi Optimization. Gurobi, 2008

work page 2008
[29]

Communication to Pine’s author, 2025

Personal communication. Communication to Pine’s author, 2025

work page 2025
[30]

Cousot and R

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. InPOPL, pages 238–252. ACM, 1977

work page 1977
[31]

Daisy - framework for analysis and optimization of numerical programs (tool paper)

Eva Darulova, Anastasiia Izycheva, Fariha Nasir, Fabian Ritter, Heiko Becker, and Robert Bastian. Daisy - framework for analysis and optimization of numerical programs (tool paper). InTools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and P...

work page 2018
[32]

Modular optimization-based roundoff error analysis of floating-point programs

Rosa Abbasi and Eva Darulova. Modular optimization-based roundoff error analysis of floating-point programs. In Static Analysis - 30th International Symposium, SAS 2023, Cascais, Portugal, October 22-24, 2023, Proceedings, volume 14284 ofLecture Notes in Computer Science, pages 41–64. Springer, 2023

work page 2023
[33]

Scaling up roundoff analysis of functional data structure programs

Anastasia Isychev and Eva Darulova. Scaling up roundoff analysis of functional data structure programs. In Static Analysis - 30th International Symposium, SAS 2023, Cascais, Portugal, October 22-24, 2023, Proceedings, volume 14284 ofLecture Notes in Computer Science, pages 371–402. Springer, 2023. 22 Invariant Generation for Floating-Point Programs via Co...

work page 2023
[34]

For degree 2, we obtain: [1, x, i, x2, xi, i2] 23 Invariant Generation for Floating-Point Programs via Constraint Solving

Variable Combination Generation:Given the two variables x and i, we can generate a list of variable combinations up to a specified degree. For degree 2, we obtain: [1, x, i, x2, xi, i2] 23 Invariant Generation for Floating-Point Programs via Constraint Solving

work page
[35]

Polynomial Template Creation:We create a polynomial template by adding a coefficient variable to each term and summing them. The degree 2 invariant template is: c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2 3.Generating Handelman Conditions:The conditionsx= 0and−1≤i≤1lead to: c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2 ≥0. This can be rewritten as: x≥0,−x≥0,1 +...

work page
[36]

The mapping from terms to degrees is: {x: 1,−x: 1,1 +i: 1,1−i: 1} leading to the additional map: {1 : 0, x 2 : 2,−x 2 : 2, x(1 +i) : 2, x(1−i) : 2,−x(1 +i) : 2,

Combining Terms:We combine the previous set to create additional correct statements up to degree 2. The mapping from terms to degrees is: {x: 1,−x: 1,1 +i: 1,1−i: 1} leading to the additional map: {1 : 0, x 2 : 2,−x 2 : 2, x(1 +i) : 2, x(1−i) : 2,−x(1 +i) : 2, . . .}

work page
[37]

According to Handelman’s theorem, this equation equals: c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2

Constructing New Polynomials:For each term generated, we add another coefficient and sum them to create a new polynomial: h[0] +h[1]x+h[2](−x) +h[3](1 +i) +h[4](1−i) +h[5](x 2) +h[6](−x 2) +h[7](x(1 +i)) +. . . According to Handelman’s theorem, this equation equals: c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2

work page
[38]

We replace each term in the variable list with a new variable: {1 :n[0], x:n[1], i:n[2], x 2 :n[3], xi:n[4], i 2 :n[5]}

Coefficient Generation:Using the sympy package, we expand the above equation and generate the coefficients for each term. We replace each term in the variable list with a new variable: {1 :n[0], x:n[1], i:n[2], x 2 :n[3], xi:n[4], i 2 :n[5]}. This simplifies the process of obtaining coefficients. We create two dictionaries, LHS and RHS, mapping terms to t...

work page
[39]

Equation System Generation:We generate the first set of equation systems by equating the values from LHS andRHSfor corresponding keys. 8.Inductive Invariant Constraint:To ensure the invariant is inductive, we impose the following constraints: −10≤x≤10, −1≤i≤1, c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2 ≥0, 1.5x−0.7x+ 1.6i−2.300740×10 −6 ≤x′ ≤1.5x−0.7x+ 1.6...

work page
[40]

24 Invariant Generation for Floating-Point Programs via Constraint Solving

Additional Equation Systems:Repeating steps 1 to 7 for the above constraint yields another set of equation systems. 24 Invariant Generation for Floating-Point Programs via Constraint Solving

work page
[41]

This leads to: c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2 ≥0 =⇒low< x <up

Optimizing the Solution:To obtain the best solution, we introduce two additional variables, low and up, to represent the lower and upper bounds forx. This leads to: c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2 ≥0 =⇒low< x <up. This implies: x≤low=⇒ −c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2 + 0.0001≥0, and x≥up=⇒ −c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2 + ...

work page
[42]

To do this, we apply all obtained solutions back to the equation system and calculate the maximum difference between the left and right sides of the equations

Final Validation:After obtaining an invariant along with its range, we must double-check that the range represents a valid solution and does not indicate a solver error. To do this, we apply all obtained solutions back to the equation system and calculate the maximum difference between the left and right sides of the equations. Additionally, we verify tha...

work page
[43]

This process is similar to step 10, but we do not need to add additional minimization

Coarse Range Check for Multiple Variables:In cases with more than one variable, we need to check the coarse range for all variables involved. This process is similar to step 10, but we do not need to add additional minimization. Instead, we set the upper and lower bounds for the other variables directly to their respective coarse upper and lower bounds by...

work page
[44]

} invariant 2 we must apply the coarse range check to both invariants to ensure that the coarse range is consistently valid throughout the execution

Handling Multiple Invariants:For benchmarks with more than one invariant, such as invariant 1 while(){ ... } invariant 2 we must apply the coarse range check to both invariants to ensure that the coarse range is consistently valid throughout the execution. These steps ensure that our invariant generation process is robust and reliable, accommodating vario...

work page

[1] [1]

Blanchet, P

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. InPLDI, pages 196–207. ACM Press, 2003

work page 2003

[2] [2]

A. Miné. Relational abstract domains for the detection of floating-point run-time errors. InESOP, volume 2986 ofLNCS, pages 3–17. Springer, 2004

work page 2004

[3] [3]

Goubault

E. Goubault. Static analyses of the precision of floating-point operations. InSAS, volume 2126 ofLNCS, pages 234–259. Springer, 2001. 20 Invariant Generation for Floating-Point Programs via Constraint Solving

work page 2001

[4] [4]

Goubault, M

E. Goubault, M. Martel, and S. Putot. Asserting the precision of floating-point computations: A simple abstract interpreter. InESOP, volume 2305 ofLNCS, pages 209–212. Springer, 2002

work page 2002

[5] [5]

Baranowski, Ian Briggs, Charles Jacobsen, Zvonimir Rakamari ´c, and Ganesh Gopalakrishnan

Alexey Solovyev, Marek S. Baranowski, Ian Briggs, Charles Jacobsen, Zvonimir Rakamari ´c, and Ganesh Gopalakrishnan. Rigorous estimation of floating-point round-off errors with symbolic taylor expansions.ACM Trans. Program. Lang. Syst., 41(1), 2018

work page 2018

[6] [6]

Scalable yet rigorous floating-point error analysis

Arnab Das, Ian Briggs, Ganesh Gopalakrishnan, Sriram Krishnamoorthy, and Pavel Panchekha. Scalable yet rigorous floating-point error analysis. InProceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, SC 2020, Virtual Event / Atlanta, Georgia, USA, November 9-19, 2020, page 51. IEEE/ACM, 2020

work page 2020

[7] [7]

Constantinides, and Alastair F

Victor Magron, George A. Constantinides, and Alastair F. Donaldson. Certified roundoff error bounds using semidefinite programming.ACM Trans. Math. Softw., 43(4):34:1–34:31, 2017

work page 2017

[8] [8]

Counterexample- and simulation-guided floating-point loop invariant synthesis

Anastasiia Izycheva, Eva Darulova, and Helmut Seidl. Counterexample- and simulation-guided floating-point loop invariant synthesis. InSAS, page 156–177. Springer-Verlag, 2020

work page 2020

[9] [9]

Moscato, Laura Titolo, Aaron Dutle, and César A

Mariano M. Moscato, Laura Titolo, Aaron Dutle, and César A. Muñoz. Automatic estimation of verified floating- point round-off errors via static analysis. InComputer Safety, Reliability, and Security - 36th International Conference, SAFECOMP 2017, Trento, Italy, September 13-15, 2017, Proceedings, pages 213–229, 2017

work page 2017

[10] [10]

Feliú, Mariano M

Laura Titolo, Marco A. Feliú, Mariano M. Moscato, and César A. Muñoz. An abstract interpretation framework for the round-off error analysis of floating-point programs. InVerification, Model Checking, and Abstract Interpre- tation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings, volume 10747 ofLecture Notes...

work page 2018

[11] [11]

Moscato, Marco A

Laura Titolo, Mariano M. Moscato, Marco A. Feliú, Paolo Masci, and César A. Muñoz. Rigorous floating-point round-off error analysis in precisa 4.0. InFormal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part II, volume 14934 ofLecture Notes in Computer Science, pages 20–38. Springer, 2024

work page 2024

[12] [12]

Floating-point tvpi abstract domain.Proc

Joao Rivera, Franz Franchetti, and Markus Püschel. Floating-point tvpi abstract domain.Proc. ACM Program. Lang., 8(PLDI), 2024

work page 2024

[13] [13]

Polynomial reachability witnesses via stellensätze

Ali Asadi, Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Mohammad Mahdavi. Polynomial reachability witnesses via stellensätze. InPLDI, pages 772–787. ACM, 2021

work page 2021

[14] [14]

Linear invariant generation using non-linear constraint solving

Michael Colón, Sriram Sankaranarayanan, and Henny Sipma. Linear invariant generation using non-linear constraint solving. InCAV, volume 2725, pages 420–432. Springer, 2003

work page 2003

[15] [15]

Sipma, and Zohar Manna

Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna. Constraint-based linear-relations analysis. InSAS, volume 3148, pages 53–68. Springer, 2004

work page 2004

[16] [16]

Polynomial invariant generation for non-deterministic recursive programs

Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Ehsan Kafshdar Goharshady. Polynomial invariant generation for non-deterministic recursive programs. PLDI 2020, page 672–687. Association for Computing Machinery, 2020

work page 2020

[17] [17]

Scalable linear invariant generation with farkas’ lemma.Proc

Hongming Liu, Hongfei Fu, Zhiyong Yu, Jiaxin Song, and Guoqiang Li. Scalable linear invariant generation with farkas’ lemma.Proc. ACM Program. Lang., 6:204–232, 2022

work page 2022

[18] [18]

Synthesizing invariants for polynomial programs by semidefinite programming.CoRR abs, 47(1):1:1–1:35, 2025

Hao Wu, Qiuye Wang, Bai Xue, Naijun Zhan, Lihong Zhi, and Zhi-Hong Yang. Synthesizing invariants for polynomial programs by semidefinite programming.CoRR abs, 47(1):1:1–1:35, 2025

work page 2025

[19] [19]

Synthesizing invariant barrier certificates via difference-of-convex programming

Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, and Joost-Pieter Katoen. Synthesizing invariant barrier certificates via difference-of-convex programming. InCAV, pages 443–466. Springer, 2021

work page 2021

[20] [20]

On completeness of sdp-based barrier certificate synthesis over unbounded domains

Hao Wu, Shenghua Feng, Ting Gan, Jie Wang, Bican Xia, and Naijun Zhan. On completeness of sdp-based barrier certificate synthesis over unbounded domains. InFM, pages 248–266. Springer, 2024

work page 2024

[21] [21]

Ieee standard for binary floating point arithmetic

IEEE Computer Society. Ieee standard for binary floating point arithmetic. Technical report, ANSI/IEEE Std 745-1985, 1985

work page 1985

[22] [22]

Toward a standard benchmark format and suite for floating-point analysis

Nasrine Damouche, Matthieu Martel, Pavel Panchekha, Chen Qiu, Alexander Sanchez-Stern, and Zachary Tatlock. Toward a standard benchmark format and suite for floating-point analysis. InNumerical Software Verification, pages 63–77. Springer International Publishing, 2017

work page 2017

[23] [23]

z3-solver, 2012

Microsoft Research. z3-solver, 2012

work page 2012

[24] [24]

Polyqent: A polynomial quantified entailment solver

Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Milad Saadat, Maximilian Seeliger, and DJordje vZikeli’c. Polyqent: A polynomial quantified entailment solver. 2024. 21 Invariant Generation for Floating-Point Programs via Constraint Solving

work page 2024

[25] [25]

Springer New York, 2009

Claus Scheiderer.Positivity and Sums of Squares: A Guide to Recent Results, pages 271–324. Springer New York, 2009

work page 2009

[26] [26]

Pysmt: A python library for satisfiability modulo theories, 2022

Pysmt Contributors. Pysmt: A python library for satisfiability modulo theories, 2022

work page 2022

[27] [27]

Amplpy: An interface to access the features of ampl from within python, 2021

AMPLpy Contributors. Amplpy: An interface to access the features of ampl from within python, 2021

work page 2021

[28] [28]

Gurobi, 2008

LLC Gurobi Optimization. Gurobi, 2008

work page 2008

[29] [29]

Communication to Pine’s author, 2025

Personal communication. Communication to Pine’s author, 2025

work page 2025

[30] [30]

Cousot and R

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. InPOPL, pages 238–252. ACM, 1977

work page 1977

[31] [31]

Daisy - framework for analysis and optimization of numerical programs (tool paper)

Eva Darulova, Anastasiia Izycheva, Fariha Nasir, Fabian Ritter, Heiko Becker, and Robert Bastian. Daisy - framework for analysis and optimization of numerical programs (tool paper). InTools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and P...

work page 2018

[32] [32]

Modular optimization-based roundoff error analysis of floating-point programs

Rosa Abbasi and Eva Darulova. Modular optimization-based roundoff error analysis of floating-point programs. In Static Analysis - 30th International Symposium, SAS 2023, Cascais, Portugal, October 22-24, 2023, Proceedings, volume 14284 ofLecture Notes in Computer Science, pages 41–64. Springer, 2023

work page 2023

[33] [33]

Scaling up roundoff analysis of functional data structure programs

Anastasia Isychev and Eva Darulova. Scaling up roundoff analysis of functional data structure programs. In Static Analysis - 30th International Symposium, SAS 2023, Cascais, Portugal, October 22-24, 2023, Proceedings, volume 14284 ofLecture Notes in Computer Science, pages 371–402. Springer, 2023. 22 Invariant Generation for Floating-Point Programs via Co...

work page 2023

[34] [34]

For degree 2, we obtain: [1, x, i, x2, xi, i2] 23 Invariant Generation for Floating-Point Programs via Constraint Solving

Variable Combination Generation:Given the two variables x and i, we can generate a list of variable combinations up to a specified degree. For degree 2, we obtain: [1, x, i, x2, xi, i2] 23 Invariant Generation for Floating-Point Programs via Constraint Solving

work page

[35] [35]

Polynomial Template Creation:We create a polynomial template by adding a coefficient variable to each term and summing them. The degree 2 invariant template is: c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2 3.Generating Handelman Conditions:The conditionsx= 0and−1≤i≤1lead to: c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2 ≥0. This can be rewritten as: x≥0,−x≥0,1 +...

work page

[36] [36]

The mapping from terms to degrees is: {x: 1,−x: 1,1 +i: 1,1−i: 1} leading to the additional map: {1 : 0, x 2 : 2,−x 2 : 2, x(1 +i) : 2, x(1−i) : 2,−x(1 +i) : 2,

Combining Terms:We combine the previous set to create additional correct statements up to degree 2. The mapping from terms to degrees is: {x: 1,−x: 1,1 +i: 1,1−i: 1} leading to the additional map: {1 : 0, x 2 : 2,−x 2 : 2, x(1 +i) : 2, x(1−i) : 2,−x(1 +i) : 2, . . .}

work page

[37] [37]

According to Handelman’s theorem, this equation equals: c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2

Constructing New Polynomials:For each term generated, we add another coefficient and sum them to create a new polynomial: h[0] +h[1]x+h[2](−x) +h[3](1 +i) +h[4](1−i) +h[5](x 2) +h[6](−x 2) +h[7](x(1 +i)) +. . . According to Handelman’s theorem, this equation equals: c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2

work page

[38] [38]

We replace each term in the variable list with a new variable: {1 :n[0], x:n[1], i:n[2], x 2 :n[3], xi:n[4], i 2 :n[5]}

Coefficient Generation:Using the sympy package, we expand the above equation and generate the coefficients for each term. We replace each term in the variable list with a new variable: {1 :n[0], x:n[1], i:n[2], x 2 :n[3], xi:n[4], i 2 :n[5]}. This simplifies the process of obtaining coefficients. We create two dictionaries, LHS and RHS, mapping terms to t...

work page

[39] [39]

Equation System Generation:We generate the first set of equation systems by equating the values from LHS andRHSfor corresponding keys. 8.Inductive Invariant Constraint:To ensure the invariant is inductive, we impose the following constraints: −10≤x≤10, −1≤i≤1, c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2 ≥0, 1.5x−0.7x+ 1.6i−2.300740×10 −6 ≤x′ ≤1.5x−0.7x+ 1.6...

work page

[40] [40]

24 Invariant Generation for Floating-Point Programs via Constraint Solving

Additional Equation Systems:Repeating steps 1 to 7 for the above constraint yields another set of equation systems. 24 Invariant Generation for Floating-Point Programs via Constraint Solving

work page

[41] [41]

This leads to: c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2 ≥0 =⇒low< x <up

Optimizing the Solution:To obtain the best solution, we introduce two additional variables, low and up, to represent the lower and upper bounds forx. This leads to: c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2 ≥0 =⇒low< x <up. This implies: x≤low=⇒ −c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2 + 0.0001≥0, and x≥up=⇒ −c[0] +c[1]x+c[2]i+c[3]x 2 +c[4]xi+c[5]i 2 + ...

work page

[42] [42]

To do this, we apply all obtained solutions back to the equation system and calculate the maximum difference between the left and right sides of the equations

Final Validation:After obtaining an invariant along with its range, we must double-check that the range represents a valid solution and does not indicate a solver error. To do this, we apply all obtained solutions back to the equation system and calculate the maximum difference between the left and right sides of the equations. Additionally, we verify tha...

work page

[43] [43]

This process is similar to step 10, but we do not need to add additional minimization

Coarse Range Check for Multiple Variables:In cases with more than one variable, we need to check the coarse range for all variables involved. This process is similar to step 10, but we do not need to add additional minimization. Instead, we set the upper and lower bounds for the other variables directly to their respective coarse upper and lower bounds by...

work page

[44] [44]

} invariant 2 we must apply the coarse range check to both invariants to ensure that the coarse range is consistently valid throughout the execution

Handling Multiple Invariants:For benchmarks with more than one invariant, such as invariant 1 while(){ ... } invariant 2 we must apply the coarse range check to both invariants to ensure that the coarse range is consistently valid throughout the execution. These steps ensure that our invariant generation process is robust and reliable, accommodating vario...

work page