A Formal Proof of Square Root and Division Elimination in Embedded Programs

DOI10.6092/ISSN.1972-5787/3887MaRDI QIDQ5195252zbMATH OpenOpenAlexFDO

Authors Pierre Neron

Publication date 18 September 2019

Full work available at URL https://doaj.org/article/1148087c56974d28aafdf2da3c5034a2

zbMATH Keywords

arithmeticembedded systemsprogram transformation

Mathematics Subject Classification ID

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

Recommendations

• A formal proof of square root and division elimination in embedded programs
• Formal verification of square root algorithms
• Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation)
• A certifying square root and division elimination
• Eliminating proofs from programs
• Hardware-Dependent Proofs of Numerical Programs
• Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
• Proofs as efficient programs

Cited in

(3)

• A certifying square root and division elimination
• A formal proof of square root and division elimination in embedded programs
• Square root and division elimination in PVS

Describes a project that uses

Uses Software

• Coq
• PVS
• HOL

This page was built for publication: A Formal Proof of Square Root and Division Elimination in Embedded Programs

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