分离逻辑断言的Coq证明策略

• 作者: 江建国 程梦奇 雷斯然
• 来源期刊: 软件工程与应用
• 学科: 教育
• 关键词: 形式化方法 程序验证 分离逻辑 COQ 交互式定理证明
• 年，卷（期）: 2020,（1）
• 页码范围: 14-21
• 页数: 8页
• 分类号: G63

摘要

大型程序的验证是一项十分复杂但又极其重要的工作。本文以使用Hoare风格的分离逻辑验证C程序为目的,在基于Coq的现有的验证系统中,添加分离蕴含以扩展其分离逻辑断言语法,使得分离逻辑断言可以更灵活的描述程序状态。此外,我们开发了一些相关的自动证明策略,尽可能的通过减少人工证明来提高验证效率。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	江建国	辽宁师范大学数学学院	17	88	4.0	9.0
2	程梦奇	辽宁师范大学数学学院	2	0	0.0	0.0
3	雷斯然	辽宁师范大学数学学院	2	0	0.0	0.0