浏览全部资源
扫码关注微信
北京交通大学智能交通数据安全与隐私保护技术北京市重点实验室,北京 100044
[ "王舜(1988-),男,陕西西安人,北京交通大学博士生,主要研究方向为形式化方法、程序分析技术、信息安全等。" ]
[ "杜晔(1978-),男,黑龙江哈尔滨人,博士,北京交通大学副教授、博士生导师,主要研究方向为网络安全、态势感知、软件可靠性分析与评估等。" ]
[ "韩臻(1962-),男,浙江宁波人,北京交通大学教授、博士生导师,主要研究方向为可信计算、系统安全、保密技术等。" ]
[ "刘吉强(1973-),男,山东海阳人,北京交通大学教授、博士生导师,主要研究方向为密码学、可信计算、隐私保护技术等。" ]
网络出版日期:2018-03,
纸质出版日期:2018-03-25
移动端阅览
王舜, 杜晔, 韩臻, 等. 基于程序局部性引导的有界模型检测优化方法[J]. 通信学报, 2018,39(3):181-190.
Shun WANG, Ye DU, Zhen HAN, et al. Locality-guided based optimization method for bounded model checker[J]. Journal on communications, 2018, 39(3): 181-190.
王舜, 杜晔, 韩臻, 等. 基于程序局部性引导的有界模型检测优化方法[J]. 通信学报, 2018,39(3):181-190. DOI: 10.11959/j.issn.1000-436x.2018050.
Shun WANG, Ye DU, Zhen HAN, et al. Locality-guided based optimization method for bounded model checker[J]. Journal on communications, 2018, 39(3): 181-190. DOI: 10.11959/j.issn.1000-436x.2018050.
基于多种模型检测方法组合的复合检测方式是当前软件模型检测领域开展研究的热点之一。在当前的研究中,提高检测的规模和检测的对象复杂程度的关键在于如何有效处理抽象的扩张和收缩。证明通过对程序模式或验证信息的利用可以加快状态空间的探索速度。面向有界模型检测(BMC)加速方法展开研究,使用程序中额外的信息和知识对其处理以协助检测器删除冗余和无效的状态。在对程序局部性进行定义的基础上,对其加速性进行讨论,提出一种加速有界检测的方法和一种改进策略,对算法进行了详细描述,并通过实验验证了方法在检测效率和性能上的优越性。
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.
JHALA R , MAJUMDAR R . Software model checking [J ] . ACM Computing Surveys , 2009 , 41 ( 4 ): 1 - 54 .
BJORNER N , MCMILLAN K , RYBALCHENKO A . On solving universally quantified horn clauses [C ] // The International Symposium on Static Analysis . 2013 : 105 - 125 .
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 .
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 .
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 .
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 .
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 .
DAVIS M , LOGEMANN G , LOVELAND D . A machine program for theorem-proving [J ] . Communications of the ACM , 1967 , 5 ( 5 ): 394 - 397 .
HOOKER J N , VINAY V . Branching rules for satisfiability [J ] . Journal of Automated Reasoning , 1995 , 15 ( 3 ): 359 - 383 .
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 .
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 .
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 .
HENZINGER T A , JHALA R , MAJUMDAR R , et al . Abstractions from proofs [J ] . ACM SIGPLAN Notices , 2004 , 39 ( 1 ): 232 - 244 .
JHALA R , MCMILLAN K L . Array abstractions from proofs [C ] // The International Conference on Computer Aided Verification . 2004 : 232 - 244 .
MCMILLAN K L , . Lazy abstraction with interpolants [C ] // The International Conference on Computer Aided Verification . 123 - 136 .
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 .
FLANAGAN C , QADEER S . Predicate abstraction for software verification [J ] . ACM SIGPLAN Notices , 2002 , 37 ( 1 ): 191 - 202 .
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 .
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 .
BEYER D , HENZINGER T A , THEODULOZ G . Lazy shape analysis [C ] // International Conference on Computer Aided Verification . 2006 : 532 - 546 .
HENZINGER T A , JHALA R , MAJUMDAR R , et al . Lazy abstraction [J ] . ACM SIGPLAN Notices , 2002 , 37 ( 1 ): 58 - 70 .
BRADLEY A R , . SAT-based model checking without unrolling [C ] // The International Conference on Verification,Model Checking,and Abstract Interpretation . 2011 : 70 - 87 .
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 .
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 .
BEYER D , KEREMOGLU M E . CPAchecker:a tool for configurable software verification [C ] // The International Conference on Computer Aided Verification . 2011 : 184 - 190 .
BEYER D , LEMBERGER T . Symbolic execution with CEGAR [M ] // Leveraging Applications of Formal Methods,Verification and Validation : Foundational Techniques.Springer International Publishing , 2016 .
BEYER D , DANGL M , WENDLER P . Boosting K-induction with Continuously-refined Invariants [M ] // Computer Aided Verification . Springer International Publishing , 2015 : 622 - 640 .
BEYER D , LOWE S . Interpolation for value analysis [J ] . Software-Engineering and Management , 2015 : 73 - 74 .
BEYER D , WENDLER P . Reuse of verification results [C ] // The International Symposium on Model Checking Software . 2013 : 1 - 17 .
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 .
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 .
KROENING D , STRICHMAN O . Decision procedures:an algorithmic point of view [M ] . Springer Publishing Company , 2008 .
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 .
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 .
0
浏览量
1102
下载量
0
CSCD
关联资源
相关文章
相关作者
相关机构