A Hoare-like proof system for analysing the computation time of programs

DOI10.1016/0167-6423(87)90029-3MaRDI QIDQ1091122zbMATH OpenOpenAlexFDO

Authors Hanne Riis Nielson

Publication date 1987

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0167-6423(87)90029-3

zbMATH Keywords

Hoare logicbubble sorting algorithmclock variablepartial and total correctness properties of programswhile programs

Mathematics Subject Classification ID

Searching and sorting (68P10) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 3846835
• Hoare logics for time bounds. A study in meta theory
• scientific article; zbMATH DE number 3888900
• scientific article; zbMATH DE number 17797
• scientific article; zbMATH DE number 3900131

Cited in

(9)

• Formal verification and evaluation of execution time in the envelope theory
• Time credits and time receipts in Iris
• Weakest precondition reasoning for expected run-times of probabilistic programs
• Graded Hoare logic and its categorical semantics
• Fifty years of Hoare's logic
• Hoare logics for time bounds. A study in meta theory
• Semantic foundations for cost analysis of pipeline-optimized programs
• scientific article; zbMATH DE number 3846835 (Why is no real title available?)
• Quantum weakest preconditions for reasoning about expected runtimes of quantum programs

This page was built for publication: A Hoare-like proof system for analysing the computation time of programs

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