分离逻辑断言的Coq证明策略
Tactics for Proving Separation Logic Assertions in Coq
摘要: 大型程序的验证是一项十分复杂但又极其重要的工作。本文以使用Hoare风格的分离逻辑验证C程序为目的，在基于Coq的现有的验证系统中，添加分离蕴含以扩展其分离逻辑断言语法，使得分离逻辑断言可以更灵活的描述程序状态。此外，我们开发了一些相关的自动证明策略，尽可能的通过减少人工证明来提高验证效率。
Abstract: The verification of the correctness of large programs is an unmanageable but important endeavor. We are interested in verifying C programs with formal methods; the logic is separation logic, a Hoare-style program logic. In this paper, we present a simple extension of the syntax of separation logic assertion on existing verification system in Coq proof assistant to make assertions more ver-satile and flexible to describe the state of programs. Moreover, we develop several tactics for prov-ing some related assertions to reduce manual proof as much as possible and improve the efficiency of verification.
文章引用：雷斯然, 程梦奇, 江建国. 分离逻辑断言的Coq证明策略[J]. 软件工程与应用, 2020, 9(1): 14-21. https://doi.org/10.12677/SEA.2020.91003

参考文献

[1] Hill, J. and Tilley, S. (2010) Creating Safety Requirement Traceability for Assuring and Recertifying Legacy Safe-ty-Critical Systems. 2010 18th IEEE International Requirements Engineering Conference, Sydney, 27 September-1 October 2010, 297-302. [Google Scholar] [CrossRef] 
[2] Hoare, C.A.R. (1969) An Axiomatic Basis for Computer Programming. Communications of the ACM, 12, 576-580.
[3] O’Hearn, P.W., Reynolds, J.C. and Yang, H. (2001) Local Reasoning about Programs that Alter Data Structures. In: Fribourg, L., Ed., Computer Science Logic. CSL 2001. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 1-19. [Google Scholar] [CrossRef] 
[4] Reynolds, J.C. (2002) Separation Logic: A Logic for Shared Mu-table Data Structures. Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, Copenhagen, 22-25 July 2002, 55-74. [Google Scholar] [CrossRef] 
[5] Chlipala, A. (2013) The Bedrock Structured Programming System: Combining Generative Metaprogramming and Hoare Logic in an Extensible Program Verifier. Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, September 2013, 391-402. [Google Scholar] [CrossRef] 
[6] Jensen, J.B., Benton, N. and Kennedy, A. (2013) High-Level Separation Logic for Low-Level Code. ACM SIGPLAN Notices, 48, 301-314. [Google Scholar] [CrossRef] 
[7] Krebbers, R. (2015) The C Standard Formalized in Coq. Ph.D. Dissertation, Radboud University, Gelderland.
[8] Sergey, I., Nanevski, A. and Banerjee, A. (2015) Mechanized Verification of Fine-Grained Concurrent Programs. ACM SIGPLAN Notices, 50, 77-87.
[9] Tuch, H., Klein, G. and Norrish, M. (2007) Types, Bytes, and Separation Logic. ACM SIGPLAN Notices, 42, 97-108. [Google Scholar] [CrossRef] 
[10] The Coq Development Team: The Coq Proof Assistant.
http://coq.inria.fr
[11] Cao, Q., Beringer, L., Gruetter, S., Dodds, J. and Appel, A.W. (2018) VST-Floyd: A Sep-aration Logic Tool to Verify Correctness of C Programs. Journal of Automated Reasoning, 61, 367-422. [Google Scholar] [CrossRef] 
[12] McCreigh, A. (2009) Practical Tactics for Separation Logic. In: Berghofer, S., Nipkow, T., Urban, C. and Wenzel, M., Eds., Theorem Proving in Higher Order Logics. TPHOLs 2009. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 343-358. [Google Scholar] [CrossRef] 
[13] Bengtson, J., Jensen, J.B. and Birkedal, L. (2012) Charge-A Framework for Higher-Order Separation Logic in Coq. In: Beringer, L. and Felty, A., Eds., Interactive Theorem Proving. ITP 2012. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 315-331. [Google Scholar] [CrossRef] 
[14] Leroy, X. (2006) Formal Certification of a Complier Back-End, or: Programming a Complier with a Proof Assistant. Proceedings of the 33th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, SC, 11-13 January 2006, 42-54. [Google Scholar] [CrossRef] 
[15] Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S. and Leroy, X. (2014) Program Logics for Certified Compilers. University of Cambridge Press, New York.
[16] Delahaye, D. (2000) A Tactic Language for the System Coq. In: Parigot, M. and Voronkov, A., Eds., Logic for Programming and Automated Reasoning. LPAR 2000. Lecture Notes in Artificial Intelligence, Springer, Berlin, Heidelberg, 85-95. [Google Scholar] [CrossRef] 
[17] Cao, J., Fu, M. and Feng, X. (2015) Practical Tactics for Verifying C Programs in Coq. Proceedings of the 2015 Conference on Certified Programs and Proofs, Mumbai, India, 15-17 January 2015, 97-108. [Google Scholar] [CrossRef] 

为你推荐