Specifying Imperative ML-Like Programs Using Dynamic Logic

DOI10.1007/978-3-642-18070-5_9zbMath1308.68044OpenAlexW2173116115MaRDI QIDQ3067541

Reiner Hähnle, Séverine Maingaud, Vincent Balat, Alexandre Miquel, Richard Bubel

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_9

zbMATH Keywords

program specificationdynamic logicMLprogram verificationKeYAF2

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

• PAF!
• KIV

Cites Work

• Unnamed Item
• Unnamed Item
• Effective interactive proofs for higher-order imperative programs
• A Hoare Logic for Call-by-Value Functional Programs
• Sequential, Parallel, and Quantified Updates of First-Order Structures
• An axiomatic basis for computer programming
• Types for Proofs and Programs