A two-phase approach for conditional floating-point verification
From MaRDI portal
Publication:2233493
DOI10.1007/978-3-030-72013-1_3zbMath1474.68191OpenAlexW3136673411MaRDI QIDQ2233493
Maria Christakis, Eva Darulova, Debasmita Lohar, Joshua Sobel, Clothilde Jeangoudoux
Publication date: 18 October 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-72013-1_3
Roundoff error (65G50) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Unnamed Item
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Deciding floating-point logic with abstract conflict driven clause learning
- A formal analysis of the compact position reporting algorithm
- A parameterized floating-point formalizaton in HOL Light
- Automatic detection of floating-point exceptions
- Static Analysis of Finite Precision Computations
- Certified Roundoff Error Bounds Using Semidefinite Programming
- Grammar Analysis and Parsing by Abstract Interpretation
- Introduction to Interval Analysis
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions
- Compositional may-must program analysis
- Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
- Containment control of a class of heterogeneous nonlinear multi-agent systems
- Fast polyhedra abstract domain
- Rigorous floating-point mixed-precision tuning
- Sound compilation of reals
This page was built for publication: A two-phase approach for conditional floating-point verification
