Access Hoare Logic
Logic in Computer Science
2026-04-01 v3 Cryptography and Security
Symbolic Computation
Abstract
Following Hoare's seminal invention, now called Hoare logic, to reason about correctness of computer programs, we advocate a related but fundamentally different approach to reason about access security of computer programs such as access control. We define the formalism, which we denote access Hoare logic, and present examples which demonstrate its usefulness and fundamental difference to Hoare logic. We prove soundness and completeness of access Hoare logic, and provide a link between access Hoare logic and standard Hoare logic. We also demonstrate a fundamental difference of access Hoare logic to other approaches, in particular incorrectness logic.
Cite
@article{arxiv.2511.01754,
title = {Access Hoare Logic},
author = {Arnold Beckmann and Anton Setzer},
journal= {arXiv preprint arXiv:2511.01754},
year = {2026}
}