Locality-guided based optimization method for bounded model checker

Shun WANG; Ye DU; Zhen HAN; Jiqiang LIU

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

您当前的位置：

首页 >

文章列表页 >

Locality-guided based optimization method for bounded model checker

Papers | 更新时间：2024-06-05

- Locality-guided based optimization method for bounded model checker
- Journal on Communications Vol. 39, Issue 3, Pages: 181-190(2018)
- 作者机构：
  
  北京交通大学智能交通数据安全与隐私保护技术北京市重点实验室，北京 100044
- 作者简介：
- 基金信息：
  
  Beijing Higher Education Young Elite Teacher Project(YETP0548)
- DOI：10.11959/j.issn.1000-436x.2018050
  CLC： TP311.1
- Online First：2018-03，
  
  Published：25 March 2018
- 稿件说明：
移动端阅览
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：

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）加速方法展开研究，使用程序中额外的信息和知识对其处理以协助检测器删除冗余和无效的状态。在对程序局部性进行定义的基础上，对其加速性进行讨论，提出一种加速有界检测的方法和一种改进策略，对算法进行了详细描述，并通过实验验证了方法在检测效率和性能上的优越性。

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.

关键词

Keywords

references

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 .

Views

1626

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Modeling and verifying based on timed automata of Internet of things gateway security system

Composable information flow verification for service chain based on model checking

采用遗传算法的低轨区域通信星座优化设计

Model checking of trusted cryptographic module

一种基于神经网络的矢量量化零冗余度信道编码方法

Related Author

Guoqing WANG

Lei ZHUANG

Ruimin WANG

Yu SONG

Kunli ZHANG

Jian-feng MA

Cong SUN

Di LU

Related Institution

School of Information Engineering, Zhengzhou University

School of Computer Science and Technology，Xidian University

解放军理工大学通信工程学院江苏南京210007

解放军理工大学通信工程学院

State Key Laboratory of Information Security,Institute of Software,Chinese Academy of Sciences

AI问答

⁰