Hoare-style reasoning from multiple contracts

DOI10.1007/978-3-319-66845-1_17MaRDI QIDQ5045478zbMATH OpenOpenAlexFDO

Authors Olaf Owe, Toktam Ramezanifarkhani, Elahe Fazeldehkordi

Publication date 4 November 2022

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-66845-1_17

zbMATH Keywords

adaptationcompletenesscontract-based specificationcontract-based verificationHoare logicmultiple contractssoundnessunavailable source code

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

• Reuse in Software Verification by Abstract Method Calls
• An abstract contract theory for programs with procedures
• Formal reasoning about modules, reuse and their correctness
• Hoare-style logic for unstructured programs
• Modular inference of subprogram contracts for safety checking

Cited in

(1)

• An abstract contract theory for programs with procedures

This page was built for publication: Hoare-style reasoning from multiple contracts

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