基于程序局部性引导的有界模型检测优化方法

doi:10.11959/j.issn.1000-436x.2018050

Abstract

Abstract:

For software model checking,approaches that combine with different kind of verification methods are now under research.The key to improve scale and complexity of verifiable software is handling the method for abstraction widening and strengthening wisely and precisely.To archive that,using extra knowledge that extracted from programming pattern or learned through verifying procedure to help eliminate the redundant state has been proved effective.Definition of program locality was given.It took the important role in accelerating software verification,then the strategy was raised and an algorithm was implemented to take advantage of program locality.This method exploits the features of modern BMC (bounded model checker) and scales up the capability of its power in large scale and comprehensive software modules.

Key words: model checking, BMC, software verification, locality,optimization

CLC Number:

TP311.1

Shun WANG,Ye DU,Zhen HAN,Jiqiang LIU. Locality-guided based optimization method for bounded model checker[J]. Journal on Communications, 2018, 39(3): 181-190.

Figures/Tables 3

References 34

[1]	JHALA R , MAJUMDAR R . Software model checking[J]. ACM Computing Surveys, 2009,41(4): 1-54.
[2]	BJORNER N , MCMILLAN K , RYBALCHENKO A . On solving universally quantified horn clauses[C]// The International Symposium on Static Analysis. 2013: 105-125.
[3]	CLARKE E , KROENING D , LERDA F . A tool for checking ansi-c programs[C]// The 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2004: 168-176.
[4]	CORDEIRO L , LISCHER B , MARQUES S J . SMT-based bounded model checking for embedded ANSIC software[J]. IEEE Transactions on Software Engineering, 2012,38(4): 137-148.
[5]	YANG Z , GANAI M K , GUPTA A ,et al. Efficient SAT-based bounded model checking for software verification[J]. Theoretical Computer Science, 2008,404(3): 256-274.
[6]	MERZ F , FALKE S , SINZ C . LLBMC:bounded model checking of C and C++ programs using a compiler IR[C]// The International Conference on Verified Software:Theories,Tools,Experiments. 2012: 146-161.
[7]	MORSE J , CORDEIRO D , NICOLE D ,et al. Handling unbounded loops with ESBMC 1.20[C]// The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2013: 619-622.
[8]	DAVIS M , LOGEMANN G , LOVELAND D . A machine program for theorem-proving[J]. Communications of the ACM, 1967,5(5): 394-397.
[9]	HOOKER J N , VINAY V . Branching rules for satisfiability[J]. Journal of Automated Reasoning, 1995,15(3): 359-383.
[10]	LI C M , ANBULAGAN A . Heuristics based on unit propagation for satisfiability problems[C]// The 15th International Joint Conference on Artificial Intelligence. 1997: 366-371.
[11]	MOURA D , BJORNER N . Z3:an efficient SMT solver[C]// The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2008: 337-340.
[12]	LIU L , KONG W , ANDO T . A survey of acceleration techniques for SMT-based bounded model checking[C]// The International Conference on Computer Sciences and Applications. 2013: 554-559.
[13]	HENZINGER T A , JHALA R , MAJUMDAR R ,et al. Abstractions from proofs[J]. ACM SIGPLAN Notices, 2004,39(1): 232-244.
[14]	JHALA R , MCMILLAN K L . Array abstractions from proofs[C]// The International Conference on Computer Aided Verification. 2004: 232-244.
[15]	MCMILLAN K L , . Lazy abstraction with interpolants[C]// The International Conference on Computer Aided Verification. 123-136.
[16]	GULAVANI B S , RAJAMANI S K . Counterexample driven refinement for abstract interpretation[C]// The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2006: 474-488.
[17]	FLANAGAN C , QADEER S . Predicate abstraction for software verification[J]. ACM SIGPLAN Notices, 2002,37(1): 191-202.
[18]	KOMURAVELLI A , GURFINKEL A , CHAKI S . Automatic abstraction in SMT-based unbounded software model checking[C]// The International Conference on Computer Aided Verification. 2013: 846-862.
[19]	APEL S , BEYER D , FRIEDBERGER K . Domain types:abstract- domain selection based on variable usage[C]// The International Conference on Hardware and Software:Verification and Testing. 2013: 262-278.
[20]	BEYER D , HENZINGER T A , THEODULOZ G . Lazy shape analysis[C]// International Conference on Computer Aided Verification. 2006: 532-546.
[21]	HENZINGER T A , JHALA R , MAJUMDAR R ,et al. Lazy abstraction[J]. ACM SIGPLAN Notices, 2002,37(1): 58-70.
[22]	BRADLEY A R , . SAT-based model checking without unrolling[C]// The International Conference on Verification,Model Checking,and Abstract Interpretation. 2011: 70-87.
[23]	RRADLEY A R , MANNA Z . Checking safety by inductive generalization of counterexamples to induction[C]// The International Conference on Formal Methods in Computer Aided Design. 2007: 173-180.
[24]	CHAKI S , CLARKE E M , GROCE A ,et al. Modular verification of software components in C[J]. IEEE Transactions on Software Engineering, 2004,30(6): 388-402.
[25]	BEYER D , KEREMOGLU M E . CPAchecker:a tool for configurable software verification[C]// The International Conference on Computer Aided Verification. 2011: 184-190.
[26]	BEYER D , LEMBERGER T . Symbolic execution with CEGAR[M]// Leveraging Applications of Formal Methods,Verification and Validation: Foundational Techniques.Springer International Publishing, 2016.
[27]	BEYER D , DANGL M , WENDLER P . Boosting K-induction with Continuously-refined Invariants[M]// Computer Aided Verification. Springer International Publishing, 2015: 622-640.
[28]	BEYER D , LOWE S . Interpolation for value analysis[J]. Software-Engineering and Management, 2015: 73-74.
[29]	BEYER D , WENDLER P . Reuse of verification results[C]// The International Symposium on Model Checking Software. 2013: 1-17.
[30]	BEYER D , LOWE S . Explicit-State software model checking based on CEGAR and interpolation[C]// The International Conference on Fundamental Approaches to Software Engineering. 2013: 146-162.
[31]	ALBARGHOUTHI A , GURFINKEL A , CHECHIK M . From Under-Approximations to Over-Approximations and Back[C]// The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2012: 157-172.
[32]	KROENING D , STRICHMAN O . Decision procedures:an algorithmic point of view[M]. Springer Publishing Company, 2008.
[33]	SINZ C , MERZ F , FALKE S . LLBMC:a bounded model checker for LLVM’s intermediate representation[C]// The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2012: 542-544.
[34]	BEYER D , . Status report on software verification[C]// The International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2014: 373-388.

Metrics

Recommended 0

No Suggested Reading articles found!

样本平均数	算法时间消耗/s
样本平均数	LLBMC	基础算法	改进算法
533	611	735	708
729	971	832	820
1 002	3 613	3 570	3 439
1 291	N/A	3 902	3 219
1 347	N/A	6 037	5 791

Locality-guided based optimization method for bounded model checker

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 3

References 34

Related Articles 8

Metrics

Recommended 0

样本类型	成功检测数量
样本类型	LLBMC	基础算法	改进算法
简单程序	39	44	45
条件程序	21	27	27
循环程序	17	23	23
内存操作程序	19	20	20

[1]	Weina YUAN,Qiu YAN. Channel estimation method based on compressive sensing for FBMC/OQAM system [J]. Journal on Communications, 2019, 40(12): 98-104.
[2]	Guoqing WANG,Lei ZHUANG,Ruimin WANG,Yu SONG,Kunli ZHANG. Modeling and verifying based on timed automata of Internet of things gateway security system [J]. Journal on Communications, 2018, 39(3): 63-75.
[3]	Jing YANG,Dan FAN,Yu-qing ZHANG. Adjusted automata learning algorithm for security protocol adaptive model checking [J]. Journal on Communications, 2015, 36(Z1): 266-276.
[4]	. Composable information flow verification for service chain based on model checking [J]. Journal on Communications, 2014, 35(11): 3-22.
[5]	Ning XI,Jian-feng MA,Cong SUN,Di LU,Tao ZHANG. Composable information flow verification for service chain based on model checking [J]. Journal on Communications, 2014, 35(11): 23-31.
[6]	Xiao-feng CHEN,Deng-guo FENG. Model checking of trusted cryptographic module [J]. Journal on Communications, 2010, 31(1): 59-64.
[7]	Xia LIU,Tian-long GU,Rong-sheng DONG,Yun-chuan GUO. Design and analysis of a novel fair payment protocol in mobile environments [J]. Journal on Communications, 2007, 28(4): 32-37.
[8]	Jia-jing LI,Tao WEI,Jian MAO. Method of model checking x86 executables for temporal security vulnerabilities [J]. Journal on Communications, 2007, 28(11A): 98-102.