School of Computer Science, University of Science and Technology of China, Hefei 230026, China;Software Security Laboratory, Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou 215123, China 在期刊界中查找 在百度中查找 在本站中查找
Affiliation:
Fund Project:
National Natural Science Foundation of China (61103023, 61229201, 61379039, 91318301, 61632005)
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.
[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]