我的阅读状态 （保存写回仓库，全设备同步；首次保存需输入访问令牌）

AI 速览

一句话：提出 Horntinuum，用约束 Horn 子句（CHC）驱动自主测试，实现测试的自动生成或引导。

本文题为《Horntinuum: Autonomous Testing using Constrained Horn Clauses》，作者为 Ilia Zlatkin 与 Grigory Fedyukovich。所提供的论文信息中不含摘要，因此以下内容仅依据标题作出推断，不代表原文的具体结论。从标题看，论文关注的核心问题是“自主测试”（autonomous testing），即让测试过程尽可能在无需或极少人工干预的情况下自动进行；其技术手段是约束 Horn 子句（Constrained Horn Clauses, CHC），这是一类在程序验证与归纳不变式推理中广泛使用的逻辑约束形式，通常借助 SMT 求解器进行求解。合理的推断是：论文将测试目标（如可达性、断言违反、覆盖条件）编码为 CHC，并通过求解这些子句来自动构造或筛选测试输入，从而把测试问题转化为约束求解问题。由于缺少摘要，本文无法给出关于方法细节、实现工具、基准评测与实验结果的可靠描述。

问题

如何以尽量自主、少人工干预的方式完成软件测试（如测试用例的自动生成与目标导向的探索）。

方法

利用约束 Horn 子句（CHC）对测试目标或程序可达性条件进行建模，并通过求解这些约束来驱动测试生成。

评估

因原文未提供摘要，无法从给定信息中确定评估方式；推测会以原型工具在基准程序上与已有测试方法的对比作为评估。

链接与引用

DOI 原文 ·

@inproceedings{paperbot7217,
  title = {Horntinuum: Autonomous Testing using Constrained Horn Clauses},
  author = {Ilia Zlatkin and Grigory Fedyukovich},
  booktitle = {ASE},
  year = {2022},
  doi = {10.1145/3551349.3563235}
}