Hoare logic and auxiliary variables
From MaRDI portal
Publication:1977126
DOI10.1007/s001650050057zbMath0978.03026OpenAlexW2142524717MaRDI QIDQ1977126
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
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
