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).

翻译：本文介绍HyperQB，一种基于QBF的按钮式超属性有界模型检验器。超属性是涉及系统多条计算轨迹的属性，涵盖众多重要的信息流安全属性和并发属性。HyperQB接收NuSMV模型和以时序逻辑HyperLTL表达的公式作为输入。与现有类似工具不同，我们基于QBF的技术使HyperQB能够无缝处理任意量词交替。用户可在两种模式间选择：错误查找（取公式非）或证据发现（取公式非否定）。我们通过一系列丰富实验案例报告了成功且高效的模型检验结果，涵盖先前已研究的案例（如信息流安全、并发数据结构、机器人规划等）以及新案例（如共终止性、可否认性及三种无干扰变体：传递性无关无干扰、终止敏感/非敏感无干扰）。