Constraint solving for interpolation

被引：25

作者：

Rybalchenko, Andrey ^{[1
]}

Sofronie-Stokkermans, Viorica ^{[2
]}

机构：

[1] Tech Univ Munich, D-8000 Munich, Germany

[2] Max Planck Inst Informat, Saarbrucken, Germany

来源：

JOURNAL OF SYMBOLIC COMPUTATION | 2010年 / 45卷 / 11期

关键词：

Interpolation; Constraint solving; Hierarchical reasoning; Program verification; LOCAL THEORY EXTENSIONS; MODEL CHECKING; ABSTRACTION REFINEMENT; LOWER BOUNDS; GENERATION; SYSTEMS; PROVER;

D O I：

10.1016/j.jsc.2010.06.005

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Interpolation is an important component of recent methods for program verification. It provides a natural and effective means for computing the separation between the sets of 'good' and 'bad' states. The existing algorithms for interpolant generation are proof-based: They require explicit construction of proofs, from which interpolants can be computed. Construction of such proofs is a difficult task. We propose an algorithm for the generation of interpolants for the combined theory of linear arithmetic and uninterpreted function symbols that does not require a priori constructed proofs to derive interpolants. It uses a reduction of the problem to constraint solving in linear arithmetic, which allows application of existing highly optimized Linear Programming solvers in a black-box fashion. We provide experimental evidence of the practical applicability of our algorithm. (C) 2010 Elsevier Ltd. All rights reserved.

引用

页码：1212 / 1233

页数：22

共 50 条

[21] Constraint Solving for Proof Planning
Jürgen Zimmer
Erica Melis
[J]. Journal of Automated Reasoning, 2004, 33 : 51 - 88
[22] A Multicore Tool for Constraint Solving
Amadini, Roberto
Gabbrielli, Maurizio
Mauro, Jacopo
[J]. PROCEEDINGS OF THE TWENTY-FOURTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI), 2015, : 232 - 238
[23] Internal constraint problem solving
不详
[J]. AUTONOMOUS DYNAMIC RECONFIGUATION IN MULT-AGENT SYSTEMS, 2002, 2427 : 167 - 189
[24] Constraints and constraint solving: An introduction
Jouannaud, JP
Treinen, R
[J]. CONSTRAINTS IN COMPUTATIONAL LOGICS: THEORY AND APPLICATIONS, 2001, 2002 : 1 - 46
[25] Adding constraint solving to Mercury
Becket, R
de la Banda, MG
Marriott, K
Somogyi, Z
Stuckey, PJ
Wallace, M
[J]. PRACTICAL ASPECTS OF DECLARATIVE LANGUAGES, 2006, 3819 : 118 - 133
[26] A Methodological View of Constraint Solving
Hubert Comon
Mehmet Dincbas
Jean-Pierre Jouannaud
Claude Kirchner
[J]. Constraints, 1999, 4 (4) : 337 - 361
[27] Constraint solving for proof planning
Zimmer, J
Melis, E
[J]. JOURNAL OF AUTOMATED REASONING, 2004, 33 (01) : 51 - 88
[28] NEURAL LOGIC CONSTRAINT SOLVING
MONFROGLIO, A
[J]. JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 1994, 20 (01) : 92 - 98
[29] Model checking as constraint solving
Podelski, A
[J]. STATIC ANALYSIS, 2000, 1824 : 22 - 37
[30] Solving Necklace Constraint Problems
Flener, Pierre
Pearson, Justin
[J]. ECAI 2008, PROCEEDINGS, 2008, 178 : 520 - +

← 1 2 3 4 5 →