论文标题
有界模型检查超构成
Bounded Model Checking for Hyperproperties
论文作者
论文摘要
超专制是关联多个计算轨迹的系统的属性，包括安全性和并发性属性。本文介绍了在HyperLTL中表达的超副词的有界模型检查（BMC）算法，据我们所知，该算法是第一个这样的算法。正如LTL的经典BMC技术主要旨在查找错误一样，我们的方法还针对识别反例。 LTL的BMC减少为SAT解决，因为LTL通过检查单个痕迹描述了属性。 HyperLTL允许在轨迹上进行明确和同时定量，并描述涉及多个痕迹的属性，因此，我们的BMC方法自然会减少到QBF求解。我们报告了成功，有效的模型检查，该模型检查是在一种名为HyperQube的工具中实施的，该工具对各种案例研究进行了丰富的实验，包括安全性，并发数据结构，机器人的路径规划和测试。
Hyperproperties are properties of systems that relate multiple computation traces, including security and concurrency properties. This paper introduces a bounded model checking (BMC) algorithm for hyperproperties expressed in HyperLTL, which - to the best of our knowledge - is the first such algorithm. Just as the classic BMC technique for LTL primarily aims at finding bugs, our approach also targets identifying counterexamples. BMC for LTL is reduced to SAT solving, because LTL describes a property via inspecting individual traces. HyperLTL allows explicit and simultaneous quantification over traces and describes properties that involves multiple traces and, hence, our BMC approach naturally reduces to QBF solving. We report on successful and efficient model checking, implemented in a tool called HyperQube, of a rich set of experiments on a variety of case studies, including security, concurrent data structures, path planning for robots, and testing.
