Hoare-style reasoning from multiple contracts

DOI10.1007/978-3-319-66845-1_17zbMATH Open1498.68168OpenAlexW2747300583MaRDI QIDQ5045478FDOQ5045478

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

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

zbMATH Keywords

adaptationcompletenessHoare logicsoundnessmultiple contractscontract-based specificationcontract-based verificationunavailable source code

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)

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)