Hyper Separation Logic (extended version)

Trayan Gospodinov, Peter Müller, Thibault Dardinier

Many important functional and security properties--including non-interference, determinism, and generalized non-interference (GNI)--are hyperproperties, i.e., properties relating m…