论文标题
会议记录第9届HORN条款验证和综合条款的研讨会以及有关验证和计划转型的第10个国际研讨会
Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation
论文作者
论文摘要
这些程序包括在第9届HORN条款验证和综合的霍恩条款和第十个国际验证和计划转换的国际研讨会上发表的部分论文，均与ETAPS 2022相关。 许多程序验证和感兴趣的综合问题都可以直接使用Horn条款进行建模，而CLP和CAV社区的许多最新进展围绕着有效地解决作为Horn条款的问题。 The HCVS series of workshops aims to bring together researchers working in the communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE, IJCAR), on the topic of Horn clause based analysis, verification, and synthesis. 这些社区在不同时期，从不同的角度和HCV倡导了验证和合成的角度，以刺激相互作用，并刺激经验的富有成效的交流和整合。 VPT研讨会的目的是将研究人员聚集在计划验证和计划转换领域的领域。 这两个领域之间存在有益相互作用的巨大潜力，因为： 1）一方面，在程序转换领域开发的方法和工具，例如部分评估，折叠/展开转换和超滤波，都将成功地用于验证无限状态和参数化系统。 2）另一方面，模型检查，抽象解释，SAT和SMT求解和自动化定理已证明已用于增强程序转换技术。此外，计划转型工具的正式认证（例如自动重构工具和编译器）最近引起了极大的兴趣，提出了重大挑战。
These proceedings include selected papers presented at the 9th Workshop on Horn Clauses for Verification and Synthesis and the Tenth International Workshop on Verification and Program Transformation, both affiliated with ETAPS 2022. Many Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the CLP and CAV communities have centered around efficiently solving problems presented as Horn clauses. The HCVS series of workshops aims to bring together researchers working in the communities of Constraint/Logic Programming (e.g., ICLP and CP), Program Verification (e.g., CAV, TACAS, and VMCAI), and Automated Deduction (e.g., CADE, IJCAR), on the topic of Horn clause based analysis, verification, and synthesis. Horn clauses for verification and synthesis have been advocated by these communities in different times and from different perspectives and HCVS is organized to stimulate interaction and a fruitful exchange and integration of experiences. The aim of the VPT workshop is to bring together researchers working in the fields of Program Verification and Program Transformation. There is a great potential for beneficial interactions between these two fields because: 1) On one hand, methods and tools developed in the field of Program Transformation such as partial evaluation, fold/unfold transformations, and supercompilation, have all been applied with success for the verification of infinite state and parameterized systems. 2) On the other hand, model checking, abstract interpretation, SAT and SMT solving and automated theorem proving have been used to enhance program transformation techniques. Moreover, the formal certification of program transformation tools, such as automated refactoring tools and compilers, has recently attracted considerable interest, posed major challenges.
