HyperQB: A QBF-Based Bounded Model Checker for Hyperproperties

This paper presents HyperQB, a push-button QBF-based bounded model checker for hyperproperties. Hyperproperties are properties of systems that relate multiple computation traces, including many important information-flow security and concurrency properties. HyperQB takes as input a NuSMV model and a formula expressed in the temporal logic HyperLTL. Unlike the existing similar tools, our QBF-based technique allows HyperQB to seamlessly deal with arbitrary quantifier alternations. The user can choose between two modes: bug-hunt (with negated formula), or find witness (with non-negated formula). We report on successful and effective model checking for a rich set of experiments on a variety of case studies, including previously investigated cases such as information-flow security, concurrent data structures, robotic planning, etc., and new cases such as co-termination, deniability, and three variations of non-interference (intransitive, termination sensitive/insensitive).