使用ATHENA验证CHC可满足性

《Formal Aspects of Computing》：Validation of CHC Satisfiability with ATHENA

本文提出两层次验证方法，通过SMT求解器验证CHC模型的正确性，并检查SMT证明的合法性。使用ATHENA框架进行大规模评估，测试3个CHC求解器、5个SMT求解器和5个证明检查器，发现14个工具错误，包括模型无效和证明生成问题，证实了验证的必要性。

　　在现代软件验证领域，逻辑求解器已成为不可或缺的工具。这些求解器能够自动推理复杂逻辑公式，帮助开发者识别程序中的错误，确保其行为符合预期。然而，随着逻辑求解器功能的增强，其代码库的复杂性也随之增加，导致错误出现的频率显著上升。为了提高验证工具的可靠性，确保其输出结果的正确性，研究者们开始探索更加严谨的验证方法，以增强对求解器结果的信心。

本文提出了一种针对受限的Horn子句（CHC）求解器输出结果的两层验证方法。该方法通过结合SMT（可满足性模理论）求解器生成的证明来验证CHC模型的正确性。这种两层验证策略不仅提高了模型验证的准确性，还为验证工具提供了额外的保障。此外，研究者还开发了一个名为ATHENA的模块化评估框架，用于大规模测试该方法的有效性。通过使用三个CHC求解器、五个SMT求解器和五个证明检查器，ATHENA能够验证CHC模型的正确性，并揭示出工具中的潜在问题。

CHC求解器在验证过程中扮演着关键角色，它们能够判断一组逻辑蕴含是否可满足。然而，由于其复杂性，CHC求解器的输出结果有时会存在错误，这不仅影响了求解器本身的可靠性，也对依赖这些结果的验证工具造成了潜在风险。因此，对CHC求解器的输出进行验证变得尤为重要。现有的验证方法主要依赖于SMT求解器，但这些求解器的输出也存在不确定性，因为它们同样可能产生错误。为了确保结果的正确性，研究者们提出了一种两层验证策略，即通过SMT求解器进行模型验证，并进一步通过SMT证明进行验证。

在实际应用中，CHC求解器的输出结果需要被验证。例如，当求解器判断一个逻辑蕴含为可满足时，需要生成一个模型，并验证该模型是否确实满足所有条件。为了实现这一目标，研究者们利用SMT求解器生成验证所需的逻辑约束，并通过这些约束来验证模型的正确性。此外，SMT证明的生成和验证也为模型提供了额外的保障。然而，当前的SMT证明检查工具在某些情况下无法完全验证这些证明，因此需要进一步的研究和开发。

ATHENA框架的开发为CHC模型的验证提供了新的可能性。通过该框架，研究者能够将CHC模型与不同的SMT求解器和证明检查器进行匹配，从而提高验证的全面性和准确性。ATHENA框架的模块化设计使得它可以灵活地适应不同的验证需求，并且能够处理大量数据。此外，ATHENA框架还能够收集和分析验证过程中产生的模型和证明的大小，这有助于理解验证过程中的资源消耗情况。

在实验评估中，研究者使用了来自CHC-COMP 2024的LIA（线性整数算术）和ALIA（数组与线性整数算术结合）的基准测试案例。这些测试案例覆盖了线性和非线性的Horn子句，并且需要验证其模型和证明的正确性。实验结果表明，所提出的两层验证方法在实践中是可行的，能够有效验证CHC模型的正确性，并且揭示了多个工具中的错误。这些错误包括模型生成中的问题、证明生成中的错误以及证明检查器的限制。

此外，研究者还发现了一些SMT求解器和证明检查器的错误。例如，某些SMT求解器在处理包含数组的模型时会出现问题，而某些证明检查器在验证证明时也会遇到挑战。这些发现不仅有助于改进现有的验证工具，也强调了在现代验证工具中引入更多验证机制的必要性。

在未来的计划中，研究者希望进一步扩展该方法，使其适用于其他FOL理论，并将其嵌入到CHC验证工具中，以提高整体的可靠性。同时，他们还计划设计一种新的方法，用于验证CHC证明本身。这些方向将有助于提升验证工具的性能和准确性，为软件验证提供更加坚实的基础。

通过ATHENA框架和两层验证方法，研究者不仅验证了CHC模型的正确性，还揭示了多个工具中的潜在问题。这些发现为后续的工具改进提供了重要依据，同时也为验证工具的进一步发展指明了方向。总之，本文的研究成果对于提高逻辑求解器的可靠性、增强验证工具的准确性具有重要意义，为软件验证领域提供了新的思路和方法。