Relational abstract interpretation for the verification of 2-hypersafety properties
Máté Kovács, Helmut Seidl, Bernd Finkbeiner · 2013
Information flow properties of programs can be formalized as hyperproperties specifying the relation of multiple executions. In this paper, we therefore introduce a framework for proving 2-hypersafety properties by means of abstract interpretation. The main idea is to apply abstract interpretation on the self-compositions of the control flow graphs of programs. As a result, our method is inherently capable of analyzing relational properties of even dissimilar programs.