第九届 Horn 子句验证与综合研讨会及第十届程序验证与程序变换国际研讨会会议论文集
编程语言
2022-11-22 v1 计算机科学中的逻辑
符号计算
软件工程
摘要
本会议论文集收录了在第九届 Horn 子句验证与综合研讨会和第十届程序验证与程序变换国际研讨会上发表的部分精选论文，两者均附属于 ETAPS 2022。许多感兴趣的程验证与综合问题可直接使用 Horn 子句建模，且 CLP 与 CAV 社群近期诸多进展围绕高效求解以 Horn 子句呈现的问题展开。HCVS 系列研讨会旨在汇聚约束/逻辑编程（如 ICLP 与 CP）、程序验证（如 CAV、TACAS 与 VMCAI）以及自动演绎（如 CADE、IJCAR）社群中从事基于 Horn 子句的分析、验证与综合的研究人员。这些社群曾在不同时期从不同视角倡导将 Horn 子句用于验证与综合，而 HCVS 的组织旨在促进互动及经验的有益交流与融合。VPT 研讨会的目的是汇聚程序验证与程序变换领域的研究人员。这两个领域之间存在巨大潜在良性互动，因为：1) 一方面，程序变换领域发展出的方法与工具，如部分求值、折叠/展开变换和超编译，均已成功应用于无限状态与参数化系统的验证。2) 另一方面，模型检测、抽象解释、SAT 与 SMT 求解以及自动定理证明已被用于增强程序变换技术。此外，程序变换工具（如自动化重构工具与编译器）的形式化认证近期引起了相当关注，并带来了重大挑战。
引用
@article{arxiv.2211.10675,
title = {Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation},
author = {Geoffrey W. Hamilton and Temesghen Kahsai and Maurizio Proietti},
journal= {arXiv preprint arXiv:2211.10675},
year = {2022}
}