不同用途不同映射：一种面向中间验证语言的程序变换
软件工程
2019-01-08 v1
摘要
在基于定理证明器或SMT求解器的验证中，待验证程序通常以中间验证语言给出，如Boogie、Why或CHC。这一设定带来了新的挑战。我们研究一种预处理步骤，其扮演类似于验证中别名分析的角色，不同之处在于现在使用（数学上的）映射来建模内存或数组类型的数据对象。我们提出一种程序变换，将程序P转换为等价程序P'，从而通过验证P'而非P，减轻用例分割数量呈指数级爆炸的负担。此处，用例分割依据的是使用同一映射变量的两条语句是否独立；若独立，我们不妨使用两个不同的映射变量，从而消除用例分割的需要（这正是该程序变换背后的思想）。我们已实现该程序变换，并表明在理想情况下可避免指数级爆炸。
引用
@article{arxiv.1901.01915,
title = {Different Maps for Different Uses. A Program Transformation for Intermediate Verification Languages},
author = {Daniel Dietsch and Matthias Heizmann and Jochen Hoenicke and Alexander Nutz and Andreas Podelski},
journal= {arXiv preprint arXiv:1901.01915},
year = {2019}
}