Deductive binary code verification against source-code-level specifications

DOI10.1007/978-3-030-50995-8_3MaRDI QIDQ6487259zbMATH OpenFDO

Authors

Publication date 9 November 2022

Full work available at URL https://doi.org/10.1007/978-3-030-50995-8_3

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Verifying branch-free assembly code in Why3
• scientific article; zbMATH DE number 1374873
• scientific article; zbMATH DE number 1630129
• Embedded software verification using symbolic execution and uninterpreted functions
• A formally verified compiler back-end

Cites work

• A Brief Overview of HOL4
• A Short Presentation of Coq
• An axiomatic basis for computer programming
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Hardware-Dependent Proofs of Numerical Programs
• scientific article; zbMATH DE number 2087570 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• Verifying branch-free assembly code in Why3
• Why3 -- where programs meet provers

Cited in

(2)

• Embedded software verification using symbolic execution and uninterpreted functions
• Automatic generation and validation of instruction encoders and decoders

This page was built for publication: Deductive binary code verification against source-code-level specifications

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