微信服务号

微信订阅号

2025-4-6- 10
Home > Archive>Volume 28, Issue 4, 2017 >819-826. DOI:10.13328/j.cnki.jos.005196
PDF HTML XML Export Cite reminder
Design and Implementation of Coq Tactics Based on Z3
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61103023, 61229201, 61379039, 91318301, 61632005)

  • Article
    • | |
  • Metrics
    • |
  • Reference [18]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    Formal verification is an effective approach to construct high confidence software. Verifying the functional correctness of complex system software by manually writing proof scripts in proof assistant tools is feasible with the low degree of automation, and the verification cost is relatively high. The automatic program verifiers verify programs by taking the annotated source code as their input to generate verification conditions automatically solved by SMT solvers. This approach has a high degree of automation, but it is impossible to verify the functional correctness of the entire system software. By combining the advantage of the above two methods, this paper implements a novel Coq tactic plug-in named "smt4coq", which allows calling the Z3 SMT solver in Coq to automatically prove mathematical propositions involved with 32-bit machine integers. The new tactic improves the degree of automation and reduces the cost of manual verification.

    Reference
    [1] De Roever WP, Engelhardt K, Buth KH. Data Refinement:Model-Oriented Proof Methods and Their Comparison, Number 47. Cambridge University Press, 1998.
    [2] Liang HJ, Feng XY, Fu M. Rrely-Guarantee-Based simulation for verifying concurrent program transformations. In:Proc. of the POPL. 2012. 455-468.[doi:10.1145/2103656.2103711]
    [3] Liang HJ, Feng XY. Modular verification of linearizability with non-fixed linearization points. In:Proc. of the PLDI. 2013. 459-470.[doi:10.1145/2491956.2462189]
    [4] Liang HJ, Hoffmann J, Feng XY, Shao Z. Characterizing progress properties of concurrent objects via contextual refinements. In:Proc. of the CONCUR. 2013. 227-241.[doi:10.1007/978-3-642-40184-8_17]
    [5] Liang HJ, Feng XY, Shao Z. Compositional verification of termination-preserving refinement of concurrent programs. In:Proc. of the CSL-LICS. 2014. 65:1-65:10.[doi:10.1145/2603088.2603123]
    [6] The Coq Development Team. The Coq Proof Assistant. http://coq.inria.fr
    [7] Nipkow T, Wenzel M, Paulson L. Isabelle/HOL:A Proof Assistant for Higher-Order Logic. Berlin, Heidelberg:Springer-Verlag, 2002.
    [8] Ernie C, Markus D, Mark H, Dirk L, Michał M, Thomas S, Wolfram S, Stephan T. VCC:A practical system for verifying concurrent C. In:Proc. of the TPHOLs. 2009. 23-42.
    [9] Leino KRM. Dafny:An automatic program verifier for functional correctness. In:Proc. of the Logic for Programming, Artificial Intelligence, and Reasoning. Springer-Verlag, 2010. 348-370.[doi:10.1007/978-3-642-17511-4_20]
    [10] De Moura L, Bjørner N. Z3:An efficient SMT solver. In:Proc. of the Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, 2008. 337-340.[doi:10.1007/978-3-540-78800-3_24]
    [11] Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S. seL4:Formal verification of an OS kernel. In:Proc. of the 22nd ACM SIG OPS Symp. on Operating Systems Principles. ACM Press, 2009. 207-220.[doi:10.1145/1629575.1629596]
    [12] Godefroid P. Software model checking:The VeriSoft approach. Formal Methods in System Design, 2005,26(2):77-101.[doi:10. 1007/s10703-005-1489-x]
    [13] Gu L, Vaynberg A, Ford B, Zhong S, Costanzo D. CertiKOS:A certified kernel for secure cloud computing. In:Proc. of the 2nd Asia-Pacific Workshop on Systems. ACM Press, 2011. 3.[doi:10.1145/2103799.2103803]
    [14] Xu FW, Fu M, Feng XY, Zhang XR, Zhang H, Li ZH. A practical verification framework for preemptive OS kernels. Computer Aided Verification, 2016.[doi:10.1007/978-3-319-41540-6_4]
    [15] Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009,52(7):107-115.[doi:10.1145/1538788. 1538814]
    [16] Reynolds JC. Separation logic:A logic for shared mutable data structures. In:Proc. of the Logic in Computer Science. 2002.[doi:10.1109/LICS.2002.1029817]
    [17] SMTCoq. https://smtcoq.github.io/
    [18] coqsmtcheck. https://github.com/gmalecha/coq-smt-check
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

张恒若,付明.基于Z3的Coq自动证明策略的设计和实现.软件学报,2017,28(4):819-826

Copy
Share
Article Metrics
  • Abstract:4760
  • PDF: 7172
  • HTML: 3212
  • Cited by: 0
History
  • Received:June 20,2016
  • Revised:September 08,2016
  • Online: January 24,2017
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2033333Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063