Formal verification of numerical programs: from C annotated programs to mechanical proofs
From MaRDI portal
Publication:1949765
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
Cites work
- scientific article; zbMATH DE number 1024452 (Why is no real title available?)
- scientific article; zbMATH DE number 2087570 (Why is no real title available?)
- scientific article; zbMATH DE number 1863384 (Why is no real title available?)
- A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor
- A floating-point technique for extending the available precision
- Accuracy and Stability of Numerical Algorithms
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Floats and Ropes: A Case Study for Formal Numerical Program Verification
- Formal proof of a wave equation resolution scheme: the method error
- Fundamental conditions for \(N\)-th-order accurate lattice Boltzmann models
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven
- Modular inference of subprogram contracts for safety checking
- Multi-prover verification of floating-point programs
- Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms
- Programming Languages and Systems
- Proving Bounds on Real-Valued Functions with Computations
- Static Analysis of Numerical Algorithms
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
- Computer-assisted verification of four interval arithmetic operators
- scientific article; zbMATH DE number 1927426 (Why is no real title available?)
- 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
Describes a project that uses
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)
