HyperQube: A QBF-Based Bounded Model Checker for Hyperproperties

Hyperproperties are properties of systems that relate multiple computation traces, including many important security and concurrency properties. In this paper, we present HyperQube, a fully automated QBF-based bounded model checker for hyperproperties. HyperQube supports one-click system verification of NuSMV models with hyperproperties specified as HyperLTL logic formulas. The QBF-based technique allows HyperQube to deal with quantifier alternation. Based on the selection of either bug hunting or find witnesses, the instances of counterexamples or witnesses are also provided back to the user. We report on successful and efficient model checking using HyperQube, with a rich set of experiments on a variety of case studies, including security, concurrent data structures, path planning for robots, and testing.