Hardware-Dependent Proofs of Numerical Programs
From MaRDI portal
Publication:3100216
DOI10.1007/978-3-642-25379-9_23zbMath1350.68241OpenAlexW1880006926MaRDI QIDQ3100216
Claude Marché, Thi Minh Tuyen Nguyen
Publication date: 22 November 2011
Published in: Certified Programs and Proofs (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-00772508/file/main.pdf
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (2)
Identifying volatile numeric expressions in numeric computing applications ⋮ Verified compilation of floating-point computations
Uses Software
Cites Work
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- Proving Bounds on Real-Valued Functions with Computations
- A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor
- Automated proofs of object code for a widely used microprocessor
- Programming Languages and Systems
- Multi-Prover Verification of Floating-Point Programs
This page was built for publication: Hardware-Dependent Proofs of Numerical Programs
