A Formal Proof of Square Root and Division Elimination in Embedded Programs
No abstract available.
DOI 10.1007/978-3-642-35308-6_20
Related papers
- With a Few Square Roots, Quantum Computing Is as Easy as Pi POPL 2024
- A unified Coq framework for verifying C programs with floating-point computations CPP 2016
- Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem CPP 2019
- Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic CPP 2024
- Windmills of the minds: an algorithm for fermat's two squares theorem CPP 2022
- Verified squared: does critical software deserve verified tools? POPL 2011
- How much is in a square? Calculating functional programs with squares JFP 2025
- A fully adequate shallow embedding of the [pi]-calculus in Isabelle/HOL with mechanized syntax analysis JFP 2003