Hoare Logic for Realistically Modelled Machine Code

DOI10.1007/978-3-540-71209-1_44MaRDI QIDQ5758130zbMATH OpenOpenAlexFDO

Authors Magnus O. Myreen, Michael J. C. Gordon

Publication date 3 September 2007

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71209-1_44

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Hoare Logic for ARM Machine Code
• Hoare-style logic for unstructured programs
• High-level separation logic for low-level code
• scientific article; zbMATH DE number 1614684
• Computer Science Logic

Cited in

(17)

• Formally verifying exceptions for low-level code with separation logic
• Hoare-style logic for unstructured programs
• Parameterized synthesis for fragments of first-order logic over data words
• Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
• High-level separation logic for low-level code
• Improved tool support for machine-code decompilation in HOL4
• AUSPICE-R: automatic safety-property proofs for realistic features in machine code
• Hoare Logic for ARM Machine Code
• A Brief Overview of HOL4
• scientific article; zbMATH DE number 7378548 (Why is no real title available?)
• Highly automated formal proofs over memory usage of assembly code
• Separation Logic Tutorial
• Modular verification of SPARCv8 code
• Proving LTL Properties of Bitvector Programs and Decompiled Binaries
• Automated verification of correctness for masked arithmetic programs
• Hoare-style logic for unstructured programs
• Hoare logic for an imperative language considering some hardware limitations

Describes a project that uses

Uses Software

• HOL

This page was built for publication: Hoare Logic for Realistically Modelled Machine Code

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