第三届真实系统形式化分析模型研讨会与第六届验证与程序转换国际研讨会会议录
计算机科学中的逻辑
2018-03-26 v1 形式语言与自动机理论
编程语言
摘要
本卷包含 MARS 2018（第三届真实系统形式化分析模型研讨会）与 VPT 2018（第六届验证与程序转换国际研讨会）的联合会议录。这两个研讨会于 2018 年 4 月 20 日在希腊塞萨洛尼基共同举行，作为 ETAPS 2018（欧洲软件理论与实践联合会议）的一部分。MARS 强调建模重于验证。其旨在讨论从为现实系统的验证与分析制定形式化方法中获得的经验教训。例如：（1）选择了哪种形式化方法及其原因？（2）必须进行哪些抽象及其原因？（3）系统的重要特征是如何建模的？（4）在系统建模过程中是否出现了任何复杂情况？（5）采取了哪些措施来保证模型的准确性？我们征集了展示真实系统完整模型的论文，这些模型可为未来的比较与分析奠定基础。该研讨会的一个目的是展示不同的建模方法，并讨论每种方法的优缺点。我们鼓励提出在本研讨会上展示的系统的替代形式化描述，这应有助于促进改进的规约形式化方法的发展。VPT 旨在提供一个论坛，使程序转换和程序验证领域的学者能够充分交流思想，并加深对这两个领域之间相互作用的理解。这些相互作用在两个方向上都是有益的。一方面，程序转换领域开发的方法和工具（如部分演绎、部分求值、折叠/展开转换和超级编译）已成功应用于验证，特别是无限状态系统和参数化系统的验证。另一方面，程序验证领域开发的方法（如模型检测、抽象解释、SAT 和 SMT 求解以及自动定理证明）被用于增强程序转换技术，从而使这些技术在实践中更加强大和有用。
引用
@article{arxiv.1803.08668,
title = {Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation},
author = {John P. Gallagher and Rob van Glabbeek and Wendelin Serwe},
journal= {arXiv preprint arXiv:1803.08668},
year = {2018}
}