Specifying imperative ML-like programs using dynamic logic

DOI10.1007/978-3-642-18070-5_9MaRDI QIDQ3067541zbMATH OpenOpenAlexFDO

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

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

MLdynamic logicprogram verificationprogram specificationKeYAF2

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)

Recommendations

• scientific article; zbMATH DE number 4101151
• Dynamic logic with trace semantics
• Dynamic logic with program specifications and its relational proof system
• scientific article; zbMATH DE number 1556014
• Characteristic formulae for the verification of imperative programs

Cites work

• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• scientific article; zbMATH DE number 1556014 (Why is no real title available?)
• A Hoare Logic for Call-by-Value Functional Programs
• An axiomatic basis for computer programming
• Effective interactive proofs for higher-order imperative programs
• Sequential, Parallel, and Quantified Updates of First-Order Structures
• Types for Proofs and Programs

Cited in

(3)

• scientific article; zbMATH DE number 3999261 (Why is no real title available?)
• scientific article; zbMATH DE number 683369 (Why is no real title available?)
• PML2: integrated program verification in ML

Describes a project that uses

Uses Software

• KIV
• PAF!

This page was built for publication: Specifying imperative ML-like programs using dynamic logic

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