Journal of Computer Applications ›› 2018, Vol. 38 ›› Issue (10): 2990-2995.DOI: 10.11772/j.issn.1001-9081.2018030733
Previous Articles Next Articles
Received:
2018-04-10
Revised:
2018-05-16
Online:
2018-10-13
Published:
2018-10-10
Supported by:
贾尚坤, 贺飞
通讯作者:
贺飞
作者简介:
贾尚坤(1993-),男,山西大同人,硕士研究生,主要研究方向:概率程序、回归验证;贺飞(1980-),男,湖南永州人,副教授,博士,CCF会员,主要研究方向:抽象精化、概率模型检测、回归验证、组合验证。
基金资助:
CLC Number:
JIA Shangkun, HE Fei. Software regression verification based on witness automata[J]. Journal of Computer Applications, 2018, 38(10): 2990-2995.
贾尚坤, 贺飞. 基于证据自动机的软件回归验证[J]. 计算机应用, 2018, 38(10): 2990-2995.
Add to citation manager EndNote|Ris|BibTeX
URL: https://www.joca.cn/EN/10.11772/j.issn.1001-9081.2018030733
[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.) |
[1] | . Partial label regression algorithm integrating feature attention and residual connection [J]. Journal of Computer Applications, 0, (): 0-0. |
[2] | Shuo SUN, Wei ZHANG, Wendi FENG, Yuwei ZHANG. Automatic foreign function interface generation method based on source code analysis [J]. Journal of Computer Applications, 2024, 44(7): 2151-2159. |
[3] | Zexuan WAN, Chunli XIE, Quanrun LYU, Yao LIANG. Code clone detection based on dependency enhanced hierarchical abstract syntax tree [J]. Journal of Computer Applications, 2024, 44(4): 1259-1268. |
[4] | Xiangjie SUN, Qiang WEI, Yisen WANG, Jiang DU. Survey of code similarity detection technology [J]. Journal of Computer Applications, 2024, 44(4): 1248-1258. |
[5] | Honglei YAO, Jiqiang LIU, Endong TONG, Wenjia NIU. Network security risk assessment method for CTCS based on α-cut triangular fuzzy number and attack tree [J]. Journal of Computer Applications, 2024, 44(4): 1018-1026. |
[6] | Xiang LIU, Bei HUA, Fei LIN, Hongyuan WEI. Design and implementation of component-based development framework for deep learning applications [J]. Journal of Computer Applications, 2024, 44(2): 526-535. |
[7] | Yihan HU, Jinlian DU, Hang SU, Hongyu GAO. Domain-specific language for natural disaster risk map generation of immovable cultural heritage [J]. Journal of Computer Applications, 2024, 44(1): 152-158. |
[8] | Qihong SONG, Jianxun LIU, Haize HU, Xiangping ZHANG. Code search model based on collaborative fusion network [J]. Journal of Computer Applications, 2023, 43(12): 3896-3902. |
[9] | Wenbo LI, Bo LIU, Lingling TAO, Fen LUO, Hang ZHANG. Deep spectral clustering algorithm with L1 regularization [J]. Journal of Computer Applications, 2023, 43(12): 3662-3667. |
[10] | Jiahao ZHU, Wei ZHENG, Fengyu YANG, Xin FAN, Peng XIAO. Software quality prediction based on back propagation neural network optimized by ant colony optimization algorithm [J]. Journal of Computer Applications, 2023, 43(11): 3568-3573. |
[11] | Sheng YE, Jing WANG, Jianfeng XIN, Guiling WANG, Chenhong GUO. Dynamic evolution method for microservice composition systems in cloud-edge environment [J]. Journal of Computer Applications, 2023, 43(6): 1696-1704. |
[12] | . Software quality prediction based on ant colony optimization improved back propagation neural network [J]. Journal of Computer Applications, 0, (): 0-0. |
[13] | Zhenhua YU, Zhengqi LIU, Ying LIU, Cheng GUO. Feature selection method based on self-adaptive hybrid particle swarm optimization for software defect prediction [J]. Journal of Computer Applications, 2023, 43(4): 1206-1213. |
[14] | Teng WANG, Zheng HUO, Yaxin HUANG, Yilin FAN. Review on privacy-preserving technologies in federated learning [J]. Journal of Computer Applications, 2023, 43(2): 437-449. |
[15] | Lingling TAO, Bo LIU, Wenbo LI, Xiping HE. Controllable face editing algorithm with closed-form solution [J]. Journal of Computer Applications, 2023, 43(2): 601-607. |
Viewed | ||||||
Full text |
|
|||||
Abstract |
|
|||||