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

DOI10.1016/j.jlamp.2023.100871zbMath1512.68151OpenAlexW4360999344MaRDI QIDQ6156936

Jorge Sousa Pinto, Maria João. Frade

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

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

Cites Work

• Unnamed Item
• Unnamed Item
• First-order dynamic logic
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
• Dynamic Logic with Non-rigid Functions
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• Why3 — Where Programs Meet Provers
• An axiomatic basis for computer programming

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