Hardware-Dependent Proofs of Numerical Programs
From MaRDI portal
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
- Publication:4503919
Cites work
- scientific article; zbMATH DE number 1953021 (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
- Automated proofs of object code for a widely used microprocessor
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- 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)- Sound compilation of reals
- Identifying volatile numeric expressions in numeric computing applications
- A Formal Proof of Square Root and Division Elimination in Embedded Programs
- C-language floating-point proofs layered with VST and Flocq
- Verified compilation of floating-point computations
- Deductive binary code verification against source-code-level specifications
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- Proof producing synthesis of arithmetic and cryptographic hardware
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)
