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.

翻译：我们提出HyperQB，一种基于QBF的"一键式"超属性有界模型检验工具。HyperQB以NuSMV模型和用时序逻辑HyperLTL表达的公式为输入。基于QBF的技术使HyperQB能够无缝处理量词交替。根据反例搜索或综合两种模式的选取，工具会返回反例实例（用于否定式公式）或见证实例（用于肯定式公式的综合）。我们在涵盖信息安全流、并发数据结构、机器人路径规划、共同终止性、否认性、非干涉的非传递性以及保密保持精化等多样案例研究的丰富实验集上，报告了成功且高效的验证结果。我们还对HyperQB与现有超属性模型检验工具进行了严格对比分析。