Hoare logic and auxiliary variables

DOI10.1007/s001650050057zbMath0978.03026OpenAlexW2142524717MaRDI QIDQ1977126

Thomas Kleymann

Publication date: 15 June 2000

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s001650050057

zbMATH Keywords

Hoare logicauxiliary variablesadaptation completenessmost general formula

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (19)

Balancing the load. Leveraging a semantics stack for systems verification ⋮ Abstraction and subsumption in modular verification of C programs ⋮ Reasoning About Resources in the Embedded Systems Language Hume ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ Completeness of Hoare Logic Relative to the Standard Model ⋮ Structural operational semantics through context-dependent behaviour ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ Verification conditions for source-level imperative programs ⋮ Toward automatic verification of quantum programs ⋮ Verified software units ⋮ A program logic for resources ⋮ The spirit of ghost code ⋮ Fifty years of Hoare's logic ⋮ Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach ⋮ Building program construction and verification tools from algebraic principles ⋮ Reverse Hoare Logic ⋮ An adaptation-complete proof system for local reasoning about cloud storage systems ⋮ Model-based specification ⋮ Calculating sharp adaptation rules.

This page was built for publication: Hoare logic and auxiliary variables