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

DOI10.1007/978-3-642-35308-6_20zbMath1383.68026OpenAlexW2173119587MaRDI QIDQ4916065

Pierre Neron

Publication date: 19 April 2013

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-00924367/file/JFRarticle.pdf

zbMATH Keywords

program transformationsemanticsprogram verificationreal number arithmeticsafety critical embedded systems

Mathematics Subject Classification ID

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

Related Items (1)

A certifying square root and division elimination

Uses Software

• Coq
• PVS
• HOL

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