A verified VCGen based on dynamic logic: an exercise in meta-verification with Why3

DOI10.1016/J.JLAMP.2023.100871MaRDI QIDQ6156936zbMATH OpenOpenAlexFDO

Authors Maria João Frade, Jorge Sousa Pinto

Publication date 19 June 2023

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.2023.100871

zbMATH Keywords

Hoare logicprogram verificationweakest preconditionsupdatesprogram annotationsverification conditions

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 4101151
• Rewriting logic as a framework for generic verification tools
• scientific article; zbMATH DE number 1617312
• scientific article; zbMATH DE number 107898
• A dynamic logic for unstructured programs with embedded assertions
• Runtime verification logics. A language design perspective
• scientific article; zbMATH DE number 1973214
• scientific article; zbMATH DE number 1975609

Cites work

• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1032009 (Why is no real title available?)
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• An axiomatic basis for computer programming
• Dynamic Logic with Non-rigid Functions
• First-order dynamic logic
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
• Why3 -- where programs meet provers

This page was built for publication: A verified VCGen based on dynamic logic: an exercise in meta-verification with Why3

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