Hoare-style logic for unstructured programs

DOI10.1016/J.JLAMP.2025.101099MaRDI QIDQ6847674zbMATH OpenFDO

Authors Didrik Lundberg, Roberto Guanciale, A. Lindner, Mads Dam

Publication date 9 March 2026

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.JLAMP.2025.101099

zbMATH Keywords

theorem provingHoare logicformal verificationbinary analysisprogram logics

Mathematics Subject Classification ID

Computer science (68-XX)

Cites work

• scientific article; zbMATH DE number 1956565 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• A compositional natural semantics and Hoare logic for low-level languages
• A critique of the foundations of Hoare style programming logics
• Abstracting Allocation
• An axiomatic basis for computer programming
• An axiomatic basis for proving total correctness of goto-programs
• Axiomatic approach to side effects and general jumps
• Axiomatic approach to total correctness of programs
• CakeML
• Certified assembly programming with embedded code pointers
• Folklore confirmed
• Goto statements: Semantics and deduction systems
• Hoare Logic for Realistically Modelled Machine Code
• Hoare-style logic for unstructured programs
• Modular verification of SPARCv8 code
• Program proving: KJumps and functions
• Programming Languages and Systems
• Refinement-Based Verification of Communicating Unstructured Code
• Soundness and Completeness of an Axiom System for Program Verification
• Validation of abstract side-channel models for computer architectures
• Verification, Model Checking, and Abstract Interpretation
• Verified just-in-time compiler on x86

This page was built for publication: Hoare-style logic for unstructured programs

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