A Dynamic Logic for Unstructured Programs with Embedded Assertions

DOI10.1007/978-3-642-18070-5_12zbMath1308.68050OpenAlexW1594807390MaRDI QIDQ3067545

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) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

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

Cites Work

• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• A Polymorphic Intermediate Verification Language: Design and Logical Encoding
• Unnamed Item

This page was built for publication: A Dynamic Logic for Unstructured Programs with Embedded Assertions