Abstract: 

Following Toni Hoare's seminal invention to reason about computer programs, which is now called Hoare logic, we introduce a related approach to reason about security properties like access control of computer programs. We will define our formalism, state main properties, and explain its connection to weakest preconditions wrt Hoare Logic. We will also present examples to illustrate our point.

This is joint work with Anton Setzer.