Relaxed stratification: A new approach to practical complete predicate refinement

Tachio Terauchi, Hiroshi Unno

研究成果

1 被引用数 (Scopus)

抄録

In counterexample-guided abstraction refinement, a predicate refinement scheme is said to be complete for a given theory if it is guaranteed to eventually find predicates sufficient to prove the given property, when such exist. However, existing complete methods require deciding if a proof of the counterexample’s spuriousness exists in some finite language of predicates. Such an exact finite-language-restricted predicate search is quite hard for many theories used in practice and incurs a heavy overhead. In this paper, we address the issue by showing that the language restriction can be relaxed so that the refinement process is restricted to infer proofs from some finite language Lbase ∪ Lext but is only required to return a proof when the counterexample’s spuriousness can be proved in Lbase. Then, we show how a proof-based refinement algorithm can be made to satisfy the relaxed requirement and be complete by restricting only the theory-level reasoning in SMT to emit Lbase -restricted partial interpolants (while such an approach has been proposed previously, we show for the first time that it can be done for languages that are not closed under conjunctions and disjunctions). We also present a technique that uses a property of counterexample patterns to further improve the efficiency of the refinement algorithm while still satisfying the requirement.We have experimented with a prototype implementation of the new refinement algorithm, and show that it is able to achieve complete refinement with only a small overhead.

本文言語English
ホスト出版物のタイトルProgramming Languages and Systems - 24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings
編集者Jan Vitek
出版社Springer Verlag
ページ610-633
ページ数24
ISBN(電子版)9783662466681
DOI
出版ステータスPublished - 2015
外部発表はい
イベント24th European Symposium on Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 - London, United Kingdom
継続期間: 2015 4 112015 4 18

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
9032
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

Conference

Conference24th European Symposium on Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
国/地域United Kingdom
CityLondon
Period15/4/1115/4/18

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「Relaxed stratification: A new approach to practical complete predicate refinement」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル