Hardware-Dependent Proofs of Numerical Programs

DOI10.1007/978-3-642-25379-9_23MaRDI QIDQ3100216zbMATH OpenOpenAlexFDO

Authors Thi Minh Tuyen Nguyen, Claude Marché

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 139821
• The notion of proof in hardware verification
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• Formal verification of arithmetic masking in hardware and software
• Multi-prover verification of floating-point programs
• Proof producing synthesis of arithmetic and cryptographic hardware
• Structuring and automating hardware proofs in a higher-order theorem- proving environment
• scientific article; zbMATH DE number 1507199

Cites work

• 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
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• scientific article; zbMATH DE number 1953021 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Multi-prover verification of floating-point programs
• Programming Languages and Systems
• Proving Bounds on Real-Valued Functions with Computations

Cited in

(8)

• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• Identifying volatile numeric expressions in numeric computing applications
• Verified compilation of floating-point computations
• Proof producing synthesis of arithmetic and cryptographic hardware
• C-language floating-point proofs layered with VST and Flocq
• A Formal Proof of Square Root and Division Elimination in Embedded Programs
• Sound compilation of reals
• Deductive binary code verification against source-code-level specifications

Describes a project that uses

Uses Software

• KRAKATOA
• JML
• Caduceus
• z3
• Spec#
• ASTREE
• cvc3
• Why3

This page was built for publication: Hardware-Dependent Proofs of Numerical Programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3100216)