We introduce the tool HyperQB 2.0, the first highly efficient push-button bounded model checker (BMC) for hyperproperties. HyperQB takes as input a model in NuSMV or Verilog and a formula expressed in the temporal logics HyperLTL or A-HLTL. The core decision procedures to implement BMC are SMT and QBF solvers, enabling verification of finite- and infinite-state programs. HyperQB offers command-line and standalone graphical, and web-based interfaces. Based on the selection of either bug-hunting or synthesis, instances of counterexamples or path witnesses are returned. The tool is entirely implemented in Rust and we report on successful and effective model checking results for a rich set of experiments on a variety of case studies with rigorous performance comparison and contrast with similar tools.

翻译：本文介绍工具HyperQB 2.0，这是首个高效的全自动有界模型检验器，专用于超属性验证。HyperQB以NuSMV或Verilog语言描述的模型及HyperLTL或A-HLTL时序逻辑公式作为输入。其核心决策过程基于SMT与QBF求解器，可实现对有限状态与无限状态程序的验证。该工具提供命令行、独立图形界面及基于Web的交互方式。根据用户选择的错误检测或综合模式，系统将返回反例实例或路径见证。本工具完全采用Rust语言实现，我们通过大量案例研究中的丰富实验，结合严格的性能对比分析与同类工具的比较，报告了成功且高效的模型检验结果。