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

DOI10.1007/978-3-030-65474-0_8MaRDI QIDQ2233532zbMATH OpenOpenAlexFDO

Authors Anastasiia Izycheva, Eva Darulova, Helmut Seidl

Publication date 18 October 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-65474-0_8

zbMATH Keywords

simulationfloating-point arithmeticinvariant synthesisCEGIS

Mathematics Subject Classification ID

Roundoff error (65G50) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• A two-phase approach for conditional floating-point verification
• Synthesis of Rigorous Floating-Point Predicates
• Loop invariants in floating point algorithms
• Formal verification of floating-point hardware design. A mathematical approach
• Numerical Software with Result Verification
• Verified compilation of floating-point computations
• Automating the verification of floating-point programs
• Formal verification of the VAMP floating point unit

Cites work

• scientific article; zbMATH DE number 3610766 (Why is no real title available?)
• A data driven approach for algebraic loop invariants
• Abstract interpretation with higher-dimensional ellipsoids and conic extrapolation
• Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
• Feedback systems: an introduction for scientists and engineers.
• Grammar Analysis and Parsing by Abstract Interpretation
• Integrating Policy Iterations in Abstract Interpreters
• Learning inductive invariants by sampling from frequency distributions
• Non-linear loop invariant generation using Gröbner bases
• Numerical invariants through convex relaxation and max-strategy iteration
• Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case
• Programming Languages and Systems
• Reasoning Algebraically About P-Solvable Loops
• Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
• SAT-Based Model Checking without Unrolling
• Solving non-linear arithmetic
• Static Analysis
• Synthesis of circular compositional program proofs via abduction
• Synthesizing invariants by solving solvable loops
• The octagon abstract domain

Cited in

(4)

• Loop invariants in floating point algorithms
• Deductive verification of floating-point Java programs in KeY
• New tools for localization of limit cycles in recursive block floating point systems
• Automatic Generation of Guard-Stable Floating-Point Code

This page was built for publication: Counterexample- and simulation-guided floating-point loop invariant synthesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233532)