.png){kind=icon}
返回
When Separation Arithmetic is Enough
.png){kind=icon}
PRE
AI
DOI：10.1007/978-3-032-10794-7_2.png)
.png){kind=icon}
.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
在演绎程序验证的实践中，希望尽可能自动化证明。目前，最好的工具是SMT求解器，能够处理一阶逻辑和线性算术。然而，SMT求解器不适合归纳推理，而归纳推理常用于处理递归数据结构，如链表或树。在本文中，我们提出了一种用于指定和证明操作基于指针的递归数据结构的命令式程序的技术，该技术保持在第一阶证明器的范围内。其思想是将递归结构映射到一个扁平的整数索引序列，以使分离和框架属性仅能通过简单的算术关系来表达。我们用两个示例来说明这种方法：一个是列表反转的一个原创变体，另一个是用于二叉树常量空间遍历的Morriss算法。
Keyword:
PROVING POINTER PROGRAMS
期刊
I
IF:
0
论文数:
23
被引数:
0
.png){kind=icon}
查看更多内容