z3 - Z3 で分離ロジックに関する推論規則を設計し、それを使用して一部の props を自動的に証明できますか?

Question

z3 の分離ロジックに関する推論規則と公理を設計し、それを使用して一部の小道具を自動的に証明できますか? たとえば、"x=y /\ (x |-> z) |- x=y /\ (y |-> z)"

Answer 1

おそらく。複数のグループが、SMT ソルバーに基づいた、またはそれらと統合された分離ロジック プルーバーに取り組んでいます。このトピックに関する最近の出版物をいくつか紹介します。

Ruzica Piskac、Thomas Wies、Damien Zufferey: SMT を使用した分離ロジックの自動化。CAV 2013

Matko Botincan、Matthew J. Parkinson、Wolfram Schulte: SMT ソルバーを使用した C プログラムの分離ロジックの検証。電気。メモ理論。計算します。科学。254

Juan Antonio Navarro Pérez、Andrey Rybalchenko: Separation Logic Modulo Theories。アプラス 2013

他にも多くのSL証明者がいると思いますが、頭のてっぺんから知っているのはSLAyerです。