A dynamic logic for unstructured programs with embedded assertions

DOI10.1007/978-3-642-18070-5_12MaRDI QIDQ3067545zbMATH OpenOpenAlexFDO

Authors Mattias Ulbrich

Publication date 21 January 2011

Published in Formal Verification of Object-Oriented Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-18070-5_12

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 4101151
• Logic programs as specifications in the inductive verification of logic programs
• Assertion based inductive verification methods for logic programs
• scientific article; zbMATH DE number 4024753
• Dynamic logic with trace semantics

Cites work

• A polymorphic intermediate verification language: design and logical encoding
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)

Cited in

(5)

• A note on undefined expression values in programming logics
• Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
• A verified VCGen based on dynamic logic: an exercise in meta-verification with Why3
• Inference rules for programming languages with side effects in expressions
• A dynamic logic for QASM programs

Describes a project that uses

Uses Software

• HOL-Boogie
• KRAKATOA
• Caduceus
• BoogiePL
• Why3
• Boogie

This page was built for publication: A dynamic logic for unstructured programs with embedded assertions

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