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能够无缝处理任意量词交替。用户可在两种模式间选择：错误检测模式（对公式取反）或证成发现模式（保持公式原样）。我们通过一系列丰富的案例研究验证了该方法的有效性与高效性，包括信息流安全、并发数据结构、机器人规划等已有案例，以及共终止性、可否认性和三种非干涉变体（传递非干涉、终止敏感/非敏感型非干涉）等新案例。