符号堆分离逻辑中的自动引理合成
计算机科学中的逻辑
2017-11-09 v3 编程语言
摘要
分离逻辑的符号堆片段已被积极开发并倡导用于验证计算机程序的内存安全属性。目前其最大挑战之一是有效证明含有归纳堆谓词的蕴含式。这些蕴含式通常是验证操作链表、树或图等复杂数据结构的程序时生成的证明义务。为辅助证明此类蕴含式，本文引入一个引理合成框架，自动发现引理以作为证明中的灵感步骤。数学归纳法与基于模板的约束求解是我们框架的两大支柱。为给定蕴含式推导支撑引理，框架首先从蕴含式的堆结构识别可能的引理模板，然后建立各模板变量间的未知关系，并进行结构归纳证明以生成关于这些关系的约束，最后求解约束以找出未知关系的实际定义，从而发现引理。我们已将该框架集成至一个原型证明器，并在多种蕴含式基准上实验。实验结果表明，我们的引理合成辅助证明器能证明许多现有方法无法处理的蕴含式。这一新方案为自动推理复杂归纳堆谓词开辟了更多机会。
引用
@article{arxiv.1710.09635,
title = {Automated Lemma Synthesis in Symbolic-Heap Separation Logic},
author = {Quang-Trung Ta and Ton Chanh Le and Siau-Cheng Khoo and Wei-Ngan Chin},
journal= {arXiv preprint arXiv:1710.09635},
year = {2017}
}