Separation Logic and Bi-Abduction for Compositional, Large-Scale Verification

[skyleaworlder]

https://www.cs.mcgill.ca/~prakash/Courses/Comp525/Talks/SL+BiAbduction.pdf

Itai Zilberstein
McGill University
November 16, 2022

from https://scholar.google.com.sg/scholar?as_sdt=0%2C5&as_vis=1&q=biabduction&btnG=

[skyleaworlder]

对这页有些存疑，论文读下来个人感觉 x -> - 指的是 x 不指向任何地址，这里表现出来有点像 “x 指向任意空间”。

这页说得很对。

[skyleaworlder]

这页的 But / Solve 意思是：正如原论文中提到的两种 Language（一种 lseg，一种带 if / while 的），某语言的 statement 种类个数是语言已经规定好的。比如 Local Reasoning 那篇论文中也提到的，每一种 statement 都可以定义其 precondition 和 postcondition。

但前后两个语句的 postcondition 与 precondition 互相推导不出来，所以语句间需要用 bi-abduction：

• 一方面是把前面一个 stmt 的 postcondition 传下去（甚至传到后面那些 stmt 去），
• 另一方面是补全前一个 stmt 的 postcondition 信息，告诉前一个 stmt 语句的 precondition 还需要的某些约束，并且把这个约束不断往前传递，甚至说传到最前面变成整个函数的约束。

于是只使用 separation logic 的 rules (Frame Rule & Sequence Rule) 也可以将两个语句的 postcondition 与 precondition 组合起来。

[skyleaworlder]

一开始利用上面的方法获得单个方法的 summary，不断迭代 summary 到收敛或超时。

在这篇 slides 里面，x -> - 表示指向任意空间，而 x -/> 表示为空。

这里定义了内存错误的 precondition / postcondition 的 specification，应用 Sequence Rule 后可以匹配出违背情况。