一句话：提出扩展符号执行以支持迹量化的全自动方法，用于发现 ∀∃ 超属性的违反。
许多重要超属性（如 refinement 和广义非干涉）属于 ∀∃ 超属性：对系统的每条执行迹，都要求存在另一条满足特定关系的迹。量词交替使这类属性极难验证甚至测试；与迹属性只需找到单一反例不同，反驳 ∀∃ 超属性既要找到一条迹，还要证明不存在与之满足指定关系的第二条迹，因而现有自动化测试工具无法覆盖。本文提出一种全自动方法，通过扩展基于符号执行的缺陷查找技术，使其支持迹量化，从而检测软件系统对 ∀∃ 超属性的违反。作者实现了原型工具，并在具有挑战性的示例集上验证了其有效性。
Many important hyperproperties, such as refinement and generalized non-interference, fall into the class of ∀∃ hyperproperties and require, for each execution trace of a system, the existence of another trace relating to the first one in a certain way. The alternation of quantifiers renders ∀∃ hyperproperties extremely difficult to verify, or even just to test. Indeed, contrary to trace properties, where it suffices to find a single counterexample trace, refuting a ∀∃ hyperproperty requires not only to find a trace, but also a proof that no second trace satisfies the specified relation with the first trace. As a consequence, automated testing of ∀∃ hyperproperties falls out of the scope of existing automated testing tools. In this paper, we present a fully automated approach to detect violations of ∀∃ hyperproperties in software systems. Our approach extends bug-finding techniques based on symbolic execution with support for trace quantification. We provide a prototype implementation of our approach, and demonstrate its effectiveness on a set of challenging examples.
@article{CorrensonNFW24,
title = {Finding ∀∃ Hyperbugs using Symbolic Execution},
author = {Arthur Correnson and Tobias Nießen and Bernd Finkbeiner and Georg Weissenbacher},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689761}
}