Bounded model checking (BMC) is an effective technique for hunting bugs by incrementally exploring the state space of a system. To reason about infinite traces through a finite structure and to ultimately obtain completeness, BMC incorporates loop conditions that revisit previously observed states. This paper focuses on developing loop conditions for BMC of HyperLTL- a temporal logic for hyperproperties that allows expressing important policies for security and consistency in concurrent systems, etc. Loop conditions for HyperLTL are more complicated than for LTL, as different traces may loop inconsistently in unrelated moments. Existing BMC approaches for HyperLTL only considered linear unrollings without any looping capability, which precludes both finding small infinite traces and obtaining a complete technique. We investigate loop conditions for HyperLTL BMC, where the HyperLTL formula can contain up to one quantifier alternation. We first present a general complete automata-based technique which is based on bounds of maximum unrollings. Then, we introduce alternative simulation-based algorithms that allow exploiting short loops effectively, generating SAT queries whose satisfiability guarantees the outcome of the original model checking problem. We also report empirical evaluation of the prototype implementation of our BMC techniques using Z3py.

翻译：有界模型检测（BMC）是一种有效的技术，通过逐步探索系统的状态空间来定位错误。为了通过有限结构推理无限轨迹并最终达到完备性，BMC引入了循环条件以重新访问先前观察到的状态。本文聚焦于为HyperLTL的BMC开发循环条件——HyperLTL是一种用于超性质的时序逻辑，能够表达并发系统中安全性和一致性等重要策略。HyperLTL的循环条件比LTL更为复杂，因为不同轨迹可能在不相关的时刻不一致地循环。现有的HyperLTL的BMC方法仅考虑无循环能力的线性展开，这既阻碍了发现小的无限轨迹，也无法实现完备技术。我们研究了HyperLTL BMC的循环条件，其中HyperLTL公式最多可包含一个量词交替。我们首先提出一种基于最大展开边界的通用完备自动化技术，然后引入基于模拟的替代算法，该算法能够有效利用短循环，生成SAT查询，其可满足性即可保证原始模型检测问题的结果。我们还报告了使用Z3py对原型实现进行的实证评估。