Abstraction refinement with Craig interpolation and symbolic pushdown systems

被引：0
|
作者：
Esparza, J [1 ]
Kiefer, S [1 ]
Schwoon, S [1 ]
机构：
[1] Univ Stuttgart, Inst Formal Methods Comp Sci, D-7000 Stuttgart, Germany
来源：
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS | 2006年 / 3920卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Counterexample-guided abstraction refinement (CEGAR) has proven to be a powerful method for software model-checking. In this paper, we investigate this concept in the context of sequential (possibly recursive) programs whose statements are given as BDDs. We examine how Craig interpolants can be computed efficiently in this case and propose a new, special type of interpolants. Moreover, we show how to treat multiple counterexamples in one refinement cycle. We have implemented this approach within the model-checker Moped and report on experiments.
引用
收藏
页码：489 / 503
页数：15
相关论文
共 50 条
  • [1] Symbolic model checking for linear hybrid systems base on craig interpolation
    Chen, Zu-Xi
    Xu, Zhong-Wei
    Huo, Wei-Wei
    Yu, Gang
    Tien Tzu Hsueh Pao/Acta Electronica Sinica, 2014, 42 (07): : 1338 - 1346
  • [2] Automatic abstraction refinement for generalized symbolic trajectory evaluation
    Chen, Yan
    He, Yujing
    Xie, Fei
    Yang, Jin
    FMCAD 2007: FORMAL METHODS IN COMPUTER AIDED DESIGN, PROCEEDINGS, 2007, : 111 - +
  • [3] Inverse Abstraction of Neural Networks Using Symbolic Interpolation
    Dathathri, Sumanth
    Gao, Sicun
    Murray, Richard M.
    THIRTY-THIRD AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE / THIRTY-FIRST INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE / NINTH AAAI SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2019, : 3437 - 3444
  • [4] Regular symbolic analysis of dynamic networks of pushdown systems
    Bouaijani, A
    Müller-Olm, M
    Touili, T
    CONCUR 2005 - CONCURRENCY THEORY, PROCEEDINGS, 2005, 3653 : 473 - 487
  • [5] Optimizing automatic abstraction refinement for Generalized Symbolic Trajectory Evaluation
    Chen, Yan
    Xie, Fei
    Yang, Jin
    2008 45TH ACM/IEEE DESIGN AUTOMATION CONFERENCE, VOLS 1 AND 2, 2008, : 143 - +
  • [6] Counterexample-guided abstraction refinement for symbolic model checking
    Clarke, E
    Grumberg, O
    Jha, S
    Lu, Y
    Veith, H
    JOURNAL OF THE ACM, 2003, 50 (05) : 752 - 794
  • [7] SAT-based assistance in abstraction refinement for Symbolic Trajectory Evaluation
    Roorda, Jan-Willem
    Claessen, Koen
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2006, 4144 : 175 - 189
  • [8] Efficient abstraction refinement in interpolation-based unbounded model checking
    Li, Bing
    Somenzi, Fabio
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2006, 3920 : 227 - 241
  • [9] Symbolic Visibly Pushdown Automata
    D'Antoni, Loris
    Alur, Rajeev
    COMPUTER AIDED VERIFICATION, CAV 2014, 2014, 8559 : 209 - 225
  • [10] Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure
    Li B.
    Wang C.
    Somenzi F.
    International Journal on Software Tools for Technology Transfer, 2005, 7 (2) : 143 - 155
12345