Some properties of programs are not about a single run of the program; instead, they relate multiple runs. For example, a program is deterministic if, given the same input, two runs will always produce the same answer. Many other properties of interest, such as security properties, are also like this. These are known as k-hyperproperties, which relate the runs of k programs.

The authors claim that current approaches to the problem are not modular, which would clearly make them difficult to scale. They instead introduce a translation-based method for verifying such properties that blows up the data dependencies (linearly in k), but does not change the control flow. Quite a bit of care is needed to design a translation that deals with each control structure appropriately.

The problem and ideas involved are well motivated through well-chosen examples (sections 2 and 3). Because of this setup, the more technical details of the construction (section 4) make sense. Section 5 is a human proof of soundness and completeness (it’s a bit surprising to see a non-mechanized proof in TOPLAS). Section 6 gives applications to various information flow and security properties, showing the wide applicability of the method, while section 7 gives a rather thorough evaluation of the corresponding implementation in Viper.

The paper is very well written and quite readable. Anyone wanting a snapshot of an interesting method for proving hyperproperties, or even learning about hyperproperties, could benefit from reading this paper.