arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 1607.01835cs.PLcs.SE
收藏

第四届验证与程序转换国际研讨会论文集

Proceedings of the Fourth International Workshop on Verification and Program Transformation

Geoff Hamilton, Alexei Lisitsa, Andrei P. Nemytykh

发表信息：
EPTCS 216, 2016
阅读 PDF
arXiv 页面 ↗HTML 原文 ↗

摘要：

本卷包含2016年4月2日在荷兰埃因霍温举行的第四届验证和程序转换国际研讨会（VPT 2016）上提交的论文的修订版。该研讨会是欧洲软件理论与实践联合会议（ETAPS 2016）的一项活动。VPT研讨会的目的是提供一个论坛，来自程序转换领域和程序验证领域的人们可以卓有成效地交换意见，并对这两个领域之间的相互作用有更深入的了解。最近在这些领域发表的研究论文表明，相互作用是非常有益的，实际上是双向的。在一个方向上，在程序转换领域中开发的方法和工具，例如部分演绎，部分求值，折叠/展开转换和超级编译，都已成功地应用于系统的验证，特别是无限状态和参数化系统的验证。在另一个方向，在程序验证，如模型检验，抽象解释，SAT和SMT解决，自动定理证明，已被用来增强程序转换技术，从而使这些技术在实践中更强大和有用的方法。

英文摘要：

This volume contains the revised versions of papers presented at the Fourth International Workshop on Verification and Program Transformation (VPT 2016) on April 2, 2016 in Eindhoven, The Netherlands. The workshop is an event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2016). The aim of the VPT workshops is to provide a forum where people from the area of program transformation and the area of program verification can fruitfully exchange ideas and gain a deeper understanding of the interactions between those two fields. The research papers which have been recently published in those fields, show that the interactions are very beneficial and, indeed, go both ways. In one direction, methods and tools developed in the field of program transformation, such as partial deduction, partial evaluation, fold/unfold transformations, and supercompilation, have all been applied with success for the verification of systems, and in particular, the verification of infinite state and parameterized systems. In the other direction, methods developed in program verification, such as model checking, abstract interpretation, SAT and SMT solving, and automated theorem proving, have been used to enhance program transformation techniques, thereby making these techniques more powerful and useful in practice.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

↑