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

DOI10.1016/J.JLAMP.2023.100871zbMATH Open1512.68151OpenAlexW4360999344MaRDI QIDQ6156936FDOQ6156936

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

Recommendations

• scientific article; zbMATH DE number 4101151
• Rewriting logic as a framework for generic verification tools
• Publication:2722043
• 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

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)

Cites Work

• Why3 -- where programs meet provers
• Title not available (Why is that?)
• First-order dynamic logic
• An axiomatic basis for computer programming
• Dynamic Logic with Non-rigid Functions
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• Title not available (Why is that?)
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach

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)