Deductive binary code verification against source-code-level specifications

DOI10.1007/978-3-030-50995-8_3zbMATH Open1511.6808MaRDI QIDQ6487259FDOQ6487259

Authors:

Publication date: 9 November 2022

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

Mathematics Subject Classification ID

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

Cites Work

• A Brief Overview of HOL4
• Why3 -- where programs meet provers
• Title not available (Why is that?)
• An axiomatic basis for computer programming
• A Short Presentation of Coq
• Title not available (Why is that?)
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Verifying branch-free assembly code in Why3
• Hardware-Dependent Proofs of Numerical Programs

Cited In (2)

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

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)