Formal verification of numerical programs: from C annotated programs to mechanical proofs

DOI10.1007/s11786-011-0099-9zbMath1264.68054OpenAlexW2141121064MaRDI QIDQ1949765

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

zbMATH Keywords

automated reasoningformal specificationfloating-point arithmeticC program

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Numerical algorithms for computer arithmetic, etc. (65Y04)

Related Items (5)

Computer-assisted verification of four interval arithmetic operators ⋮ Affine Arithmetic and Applications to Real-Number Proving ⋮ Formal analysis of the compact position reporting algorithm ⋮ A formally verified floating-point implementation of the compact position reporting algorithm ⋮ Hardware-Dependent Proofs of Numerical Programs

Uses Software

• Coq
• KRAKATOA
• ACSL
• Why3
• JML
• Spec#
• Caduceus
• mctoolbox
• Gappa
• cvc3
• z3
• ASTREE
• CIL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modular inference of subprogram contracts for safety checking
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Fundamental conditions for \(N\)-th-order accurate lattice Boltzmann models
• A floating-point technique for extending the available precision
• Proving Bounds on Real-Valued Functions with Computations
• Static Analysis of Numerical Algorithms
• 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
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor
• Accuracy and Stability of Numerical Algorithms
• Kahan's Algorithm for a Correct Discriminant Computation at Last Formally Proven
• Programming Languages and Systems
• Formal Proof of a Wave Equation Resolution Scheme: The Method Error
• Multi-Prover Verification of Floating-Point Programs

This page was built for publication: Formal verification of numerical programs: from C annotated programs to mechanical proofs