Counterexample- and simulation-guided floating-point loop invariant synthesis
From MaRDI portal
Publication:2233532
DOI10.1007/978-3-030-65474-0_8zbMath1474.68055OpenAlexW3118905376MaRDI QIDQ2233532
Helmut Seidl, Eva Darulova, Anastasiia Izycheva
Publication date: 18 October 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-65474-0_8
Roundoff error (65G50) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Cites Work
- Unnamed Item
- Unnamed Item
- The octagon abstract domain
- Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case
- Abstract interpretation with higher-dimensional ellipsoids and conic extrapolation
- Learning inductive invariants by sampling from frequency distributions
- Numerical invariants through convex relaxation and max-strategy iteration
- Solving Non-linear Arithmetic
- SAT-Based Model Checking without Unrolling
- Non-linear loop invariant generation using Gröbner bases
- Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis
- Grammar Analysis and Parsing by Abstract Interpretation
- Synthesizing Invariants by Solving Solvable Loops
- Integrating Policy Iterations in Abstract Interpreters
- Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions
- Programming Languages and Systems
- A Data Driven Approach for Algebraic Loop Invariants
- Synthesis of Circular Compositional Program Proofs via Abduction
- Reasoning Algebraically About P-Solvable Loops
- Static Analysis
