Specifying imperative ML-like programs using dynamic logic

DOI10.1007/978-3-642-18070-5_9zbMATH Open1308.68044OpenAlexW2173116115MaRDI QIDQ3067541FDOQ3067541

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

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

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)

Cites Work

• Title not available (Why is that?)
• An axiomatic basis for computer programming
• Effective interactive proofs for higher-order imperative programs
• Title not available (Why is that?)
• Sequential, Parallel, and Quantified Updates of First-Order Structures
• A Hoare Logic for Call-by-Value Functional Programs
• Types for Proofs and Programs

Cited In (3)

• Title not available (Why is that?)
• Title not available (Why is that?)
• PML2: integrated program verification in ML

Uses Software

• PAF!
• KIV

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)