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 条

[21] Constructing Craig interpolation formulas
Huang, GX
COMPUTING AND COMBINATORICS, 1995, 959 : 181 - 190
[22] Craig Interpolation in Displayable Logics
Brotherston, James
Gore, Rajeev
AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 2011, 6793 : 88 - 103
[23] Symbolic strategy synthesis for games on pushdown graphs
Cachat, T
AUTOMATA, LANGUAGES AND PROGRAMMING, 2002, 2380 : 704 - 715
[24] Symbolic execution with abstraction
Anand S.
Pǎsǎreanu C.S.
Visser W.
International Journal on Software Tools for Technology Transfer, 2009, 11 (01) : 53 - 67
[25] Parametrization of completeness in symbolic abstraction of bounded input linear systems
Adimoolam, Santosh Arvind
2014 22ND MEDITERRANEAN CONFERENCE ON CONTROL AND AUTOMATION (MED), 2014, : 978 - 983
[26] Abstraction refinement for termination
Cook, B
Podelski, A
Rybalchenko, A
STATIC ANALYSIS, PROCEEDINGS, 2005, 3672 : 87 - 101
[27] An efficient approach for abstraction-refinement verification of hybrid systems
Liu, Baoluo
Pei, Hailong
Zhang, Shengxiang
Li, Jiangqiang
2007 IEEE INTERNATIONAL CONFERENCE ON CONTROL AND AUTOMATION, VOLS 1-7, 2007, : 333 - 338
[28] Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems
Iosif, Radu
Rogalewicz, Adam
Vojnar, Tomas
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS (TACAS 2016), 2016, 9636 : 71 - 89
[29] Validation by Abstraction and Refinement
Stock, Sebastian
Vu, Fabian
Gelessus, David
Leuschel, Michael
Mashkoor, Atif
Egyed, Alexander
RIGOROUS STATE-BASED METHODS, ABZ 2023, 2023, 14010 : 160 - 178
[30] Abstraction Refinement for Stability
Duggirala, Parasara Sridhar
Mitra, Sayan
2011 ACM/IEEE SECOND INTERNATIONAL CONFERENCE ON CYBER-PHYSICAL SYSTEMS (ICCPS 2011), 2011, : 22 - 31

← 1 2 3 4 5 →