Explaining the effectiveness of small refinement heuristics in program verification with CEGAR

Tachio Terauchi*

*この研究の対応する著者

研究成果: Conference contribution

1 被引用数 (Scopus)

抄録

Safety property (i.e., reachability) verification is undecidable for Turing-complete programming languages. Nonetheless, recent progress has lead to heuristic verification methods, such as the ones based on predicate abstraction with counterexample-guided refinement (CEGAR), that work surprisingly well in practice. In this paper, we investigate the effectiveness of the small refinement heuristic which, for abstraction refinement in CEGAR, uses (the predicates in) a small proof of the given counterexample’s spuriousness [3,12,17,22]. Such a method has shown to be quite effective in practice but thus far lacked a theoretical backing. Our core result is that the heuristic guarantees certain bounds on the number of CEGAR iterations, relative to the size of a proof for the input program.

本文言語English
ホスト出版物のタイトルStatic Analysis- 22nd International Symposium, SAS 2015, Proceedings
編集者Sandrine Blazy, Thomas Jensen
出版社Springer Verlag
ページ128-144
ページ数17
ISBN(印刷版)9783662482872
DOI
出版ステータスPublished - 2015
外部発表はい
イベント22nd International Static Analysis Symposium, SAS 2015 - Saint-Malo, France
継続期間: 2015 9月 92015 9月 11

出版物シリーズ

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

Other

Other22nd International Static Analysis Symposium, SAS 2015
国/地域France
CitySaint-Malo
Period15/9/915/9/11

ASJC Scopus subject areas

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

フィンガープリント

「Explaining the effectiveness of small refinement heuristics in program verification with CEGAR」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル