Complete Bounded Model Checking for Hyperproperties
Florian Bies
Hyperproperties allow us to specify properties that relate multiple execution traces of systems with each other. The increased expressiveness comes at the cost of a significantly higher complexity of model checking. This gives rise to the development of feasible model checking algorithms that are applicable to particular fragments of hyperproperties. In this context, recent work has generalized linear temporal logic (LTL) bounded model checking (BMC) to the hyperlogic HyperLTL, an extension of LTL to multiple traces. The fundamental idea of BMC is to establish a witness by considering only trace prefixes of bounded length. But the proposed algorithm is subject to the restriction that it is unable to argue about infinite traces such that formulas involving global requirements cannot be verified. In this thesis, we attempt to eliminate this limitation. We discuss to what extent completeness techniques for LTL bounded model checking are applicable to HyperLTL. Aside from this, we develop novel approaches that are suitable to deal with trace quantification. Overall, we find ways to verify HyperLTL formulas incorporating an LTL invariant.
Bachelor Thesis.