Towards Modularly Comparing Programs Using Automated Theorem Provers
Towards Modularly Comparing Programs Using Automated Theorem Provers
复制标题
使用自动定理证明器对程序进行模块化比较
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Henrique Rebêlo
中科院分区：
文献类型：
--
作者：
C. Hawblitzel;Ming Kawaguchi;Shuvendu K. Lahiri;Henrique Rebêlo
在本文中，我们提出了一个通用的框架，用于模块化比较两个(命令式)程序，这些程序可以利用基于自动定理证明器的单程序验证器。我们将(I)相互摘要用于比较两个程序的摘要，以及(Ii)相对终止来描述两个程序相对终止的条件。这两个规则一起允许检查过程间转换的正确性。在这个框架中，我们还提供了一个处理非结构化控制流(包括循环)的通用框架。我们演示了该框架在验证等价性、编译器优化和过程间转换方面的有效性和局限性。
In this paper, we present a general framework for modularly comparing two (imperative) programs that can leverage single-program verifiers based on automated theorem provers. We formalize (i) mutual summaries for comparing the summaries of two programs, and (ii) relative termination to describe conditions under which two programs relatively terminate. The two rules together allow for checking correctness of interprocedural transformations. We also provide a general framework for dealing with unstructured control flow (including loops) in this framework. We demonstrate the usefulness and limitations of the framework for verifying equivalence, compiler optimizations, and interprocedural transformations.