Formal verification of numerical programs: from C annotated programs to mechanical proofs
DOI10.1007/S11786-011-0099-9zbMATH Open1264.68054OpenAlexW2141121064MaRDI QIDQ1949765FDOQ1949765
Authors: Sylvie Boldo, Claude Marché 
Publication date: 16 May 2013
Published in: Mathematics in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s11786-011-0099-9
Recommendations
- C-language floating-point proofs layered with VST and Flocq
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Floats and Ropes: A Case Study for Formal Numerical Program Verification
- Hardware-Dependent Proofs of Numerical Programs
Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Numerical algorithms for computer arithmetic, etc. (65Y04)
Cites Work
- Programming Languages and Systems
- Title not available (Why is that?)
- Accuracy and Stability of Numerical Algorithms
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Proving Bounds on Real-Valued Functions with Computations
- A floating-point technique for extending the available precision
- Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Floats and Ropes: A Case Study for Formal Numerical Program Verification
- Title not available (Why is that?)
- Title not available (Why is that?)
- Formal proof of a wave equation resolution scheme: the method error
- Static Analysis of Numerical Algorithms
- Multi-prover verification of floating-point programs
- A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor
- Fundamental conditions for \(N\)-th-order accurate lattice Boltzmann models
- Modular inference of subprogram contracts for safety checking
- Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven
Cited In (16)
- Semantical proofs of correctness for programs performing non-deterministic tests on real numbers
- Formal analysis of the compact position reporting algorithm
- A formally verified floating-point implementation of the compact position reporting algorithm
- C-language floating-point proofs layered with VST and Flocq
- Verifying properties of differentiable programs
- Hardware-Dependent Proofs of Numerical Programs
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Floats and Ropes: A Case Study for Formal Numerical Program Verification
- Affine arithmetic and applications to real-number proving
- Trusting computations: a mechanized proof from partial differential equations to actual program
- A formal proof of square root and division elimination in embedded programs
- Title not available (Why is that?)
- Computer-assisted verification of four interval arithmetic operators
- Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Provably correct floating-point implementation of a point-in-polygon algorithm
Uses Software
This page was built for publication: Formal verification of numerical programs: from C annotated programs to mechanical proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1949765)
