  We present HyperQB, a push-button QBF-based bounded model checker for
hyperproperties. HyperQB takes as input a NuSMV model and a formula expressed
in the temporal logic HyperLTL. Our QBF-based technique allows HyperQB to
seamlessly deal with quantifier alternations. Based on the selection of either
bug hunting or synthesis, the instances of counterexamples (for negated
formula) or witnesses (for synthesis of positive formulas) are returned. We
report on successful and effective verification for a rich set of experiments
on a variety of case studies, including information-flow security, concurrent
data structures, path planning for robots, co-termination, deniability,
intransitivity of non-interference, and secrecy-preserving refinement. We also
rigorously compare and contrast HyperQB with existing tools for model checking
hyperporperties.
