[1] BJESSE P. What is formal verification?[J]. ACM SIGDA Newsletter, 2005, 35(24):Article No. 1. [2] BEYER D, LÖWE S, NOVIKOV E, et al. Precision reuse for efficient regression verification[C]//Proceedings of the 20139th Joint Meeting on Foundations of Software Engineering. New York:ACM, 2013:389-399. [3] ROTHERMEL G, HARROLD M J. Analyzing regression test selection techniques[J]. IEEE Transactions on Software Engineering, 1996, 22(8):529-551. [4] YANG G, DWYER M B, ROTHERMEL G. Regression model checking[C]//Proceedings of the 2009 IEEE International Conference on Software Maintenance. Piscataway, NJ:IEEE, 2009:115-124. [5] GODLIN B, STRICHMAN O. Regression verification[C]//Proceedings of the 46th Annual Design Automation Conference. New York:ACM, 2009:466-471. [6] BEYER D, WENDLER P. Reuse of verification results[C]//Proceedings of the 2013 International SPIN Workshop on Model Checking of Software. Berlin:Springer, 2013:1-17. [7] BEYER D, DANGL M, DIETSCH D, et al. Correctness witnesses:exchanging verification results between verifiers[C]//Proceedings of the 201624th ACM SIGSOFT International Symposium on Foundations of Software Engineering. New York:ACM, 2016:326-337. [8] BEYER D, DANGL M, DIETSCH D, et al. Witness validation and stepwise testification across software verifiers[C]//Proceedings of the 201510th Joint Meeting on Foundations of Software Engineering. New York:ACM, 2015:721-733. [9] BEYER D. Software verification and verifiable witnesses[C]//Proceedings of the 2015 International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer, 2015:401-416. [10] BEYER D. Software verification with validation of results[C]//Proceedings of the 2017 International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer, 2017:331-349. [11] BEYER D, HENZINGER T A, THÉODULOZ G. Configurable software verification:Concretizing the convergence of model checking and program analysis[C]//Proceedings of the 2007 International Conference on Computer Aided Verification. Berlin:Springer,2007:504-518. [12] BEYER D, KEREMOGLU M E. CPAchecker:a tool for configurable software verification[C]//Proceedings of the 2011 International Conference on Computer Aided Verification. Berlin:Springer, 2011:184-190. [13] CUOQ P, KIRCHNER F, KOSMATOV N, et al. Frama-C[C]//Proceedings of the 2012 International Conference on Software Engineering and Formal Methods. Berlin:Springer, 2012:233-247. [14] SHEERAN M, SINGH S, STÅLMARCK G. Checking safety properties using induction and a SAT-solver[C]//Proceedings of the 2000 International Conference on Formal Methods in Computer-aided Design. Berlin:Springer, 2000:127-144. [15] DONALDSON A F, KROENING D, RVMMER P. Automatic analysis of DMA races using model checking and k-induction[J]. Formal Methods in System Design, 2011, 39(1):83-113. [16] HAGEN G, TINELLI C. Scaling up the formal verification of Lustre programs with SMT-based techniques[C]//Proceedings of the 2008 Formal Methods in Computer-Aided Design. Piscataway, NJ:IEEE, 2008:1-9. [17] ROCHA H, ISMAIL H, CORDEIRO L, et al. Model checking embedded C software using k-induction and invariants[M]//LETTNIN D, WINTERHOLER M. Embedded Software Verification and Debugging. Berlin:Springer, 2017:159-182. [18] BEYER D, DANGL M, WENDLER P. Boosting k-induction with continuously-refined invariants[C]//Proceedings of the 2015 International Conference on Computer Aided Verification. Berlin:Springer, 2015:622-640. [19] BEYER D, HENZINGER T A, THÉODULOZ G. Program analysis with dynamic precision adjustment[C]//Proceedings of the 200823rd IEEE/ACM International Conference on Automated Software Engineering. Washington, DC:IEEE Computer Society, 2008:29-38. [20] BEYER D, DANGL M, WENDLER P. Combining k-induction with continuously-refined invariants[EB/OL].[2018-01-02].https://arxiv.org/abs/1502.00096. [21] JIA Y, HARMAN M. MILU:a customizable, runtime-optimized higher order mutation testing tool for the full C language[C]//Proceedings of the Testing:Academic & Industrial Conference-Practice and Research Techniques. Washington, DC:IEEE Computer Society, 2008:94-98. [22] BEYER D, LÖWE S, WENDLER P. Benchmarking and resource measurement[C]//Proceedings of the 2015 International SPIN Workshop on Model Checking of Software. Berlin:Springer, 2015:160-178. [23] 杨军, 葛海通, 郑飞君, 等. 一种形式化验证方法:模型检验[J]. 浙江大学学报(理学版), 2006, 33(4):403-407. (YANG J, GE H T, ZHENG F J, et al. A formal verification method:model checking[J]. Journal of Zhejiang University (Science Edition), 2006, 33(4):403-407.) [24] 石海鹤, 肖正兴, 薛锦云. 循环不变式开发新策略及其应用[J]. 计算机工程与应用, 2006, 42(4):105-107. (SHI H H, XIAO Z X, XUE J Y. A new strategy for developing loop invariants and its application[J]. Computer Engineering and Applications, 2006, 42(4):105-107.) [25] 李未, 黄雄. 命题逻辑可满足性问题的算法分析[J]. 计算机科学, 1999, 26(3):1-9. (LI W, HUANG X. The analysis of algorithms for the propositional logic satisfiability problem[J]. Computer Science, 1999, 26(3):1-9.) |