用于指针逻辑的自动定理证明器的设计与实现的中期报告

用于指针逻辑的自动定理证明器的设计与实现的中期报告中期报告：1.背景与相关工作指针逻辑是程序验证中经常使用的一种逻辑，可以用于描述指针数据结构的不变量和程序正确性。常见的指针逻辑有Separation