A Constraint-Pattern Based Method for Reachability Determination

被引:10
作者
Wang, Yuexing [1 ,2 ,3 ]
Gu, Zuxing [1 ,2 ,3 ]
Cheng, Xi [1 ,2 ,3 ]
Zhou, Min [1 ,2 ,3 ]
Song, Xiaoyu [4 ]
Gu, Ming [1 ,2 ,3 ]
Sun, Jiaguang [1 ,2 ,3 ]
机构
[1] Minist Educ, Key Lab Informat Syst Secur, Beijing, Peoples R China
[2] Tsinghua Natl Lab Informat Sci & Technol TNList, Beijing, Peoples R China
[3] Tsinghua Univ, Sch Software, Beijing, Peoples R China
[4] Portland State Univ, Elect & Comp Engn, Portland, OR 97207 USA
来源
2017 IEEE 41ST ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 1 | 2017年
关键词
D O I
10.1109/COMPSAC.2017.12
中图分类号
TP39 [计算机的应用];
学科分类号
081203 ; 0835 ;
摘要
When analyzing programs using static program analysis, we need to determine the reachability of each possible execution path of the programs. Many static analysis tools collect constraints of each path and use SMT solvers to determine the satisfiability of these constraints. The accumulated computing time can be long if we use SMT solvers too many times. In this paper, we propose a constraint-pattern based method for reachability determination to address the limitation of current approaches. We define some constraint-patterns. For each pattern, a carefully designed constraints solving algorithm is presented. Our method contains two steps. Firstly, we collect some information about the constraints in the program to be analyzed. Then we choose the most suitable algorithm for reachability determination based on the information. Secondly, we apply the algorithm in analysis process to speed up satisfiability checking of path constraints. We implement our method based on CPAchecker, a famous software verification tool. The experimental results on some well-known benchmarks show that, with a moderate accuracy, our method is more efficient in comparison with some state-of-the-art SMT solvers.
引用
收藏
页码:85 / 90
页数:6
相关论文
共 15 条
  • [1] Barrett Clark, 2007, LNCS, P298
  • [2] BEYER D, 2007, INT C COMP AID VER, V4590, P504
  • [3] MATHSAT: Tight integration of SAT and mathematical decision procedures
    Bozzano, Marco
    Bruttomesso, Roberto
    Cimatti, Alessandro
    Junttila, Tommi
    Van Rossum, Peter
    Schulz, Stephan
    Sebastiani, Roberto
    [J]. JOURNAL OF AUTOMATED REASONING, 2005, 35 (1-3) : 265 - 293
  • [4] Brummayer R, 2009, LECT NOTES COMPUT SC, V5505, P174, DOI 10.1007/978-3-642-00768-2_16
  • [5] Static analysis for security
    Chess, B
    McGraw, G
    [J]. IEEE SECURITY & PRIVACY, 2004, 2 (06) : 76 - 79
  • [6] Cimatti A, 2013, LECT NOTES COMPUT SC, V7795, P93
  • [7] SMT-Based Bounded Model Checking for Embedded ANSI-C Software
    Cordeiro, Lucas
    Fischer, Bernd
    Marques-Silva, Joao
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2012, 38 (04) : 957 - 974
  • [8] Cousot P, 2002, LECT NOTES COMPUT SC, V2304, P159
  • [9] Z3: An efficient SMT solver
    de Moura, Leonardo
    Bjorner, Nikolaj
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 337 - 340
  • [10] Dutertre Bruno., 2006, The yices smt solver, V2, P2