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

Tachio Terauchi*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (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.

Original languageEnglish
Title of host publicationStatic Analysis- 22nd International Symposium, SAS 2015, Proceedings
EditorsSandrine Blazy, Thomas Jensen
PublisherSpringer Verlag
Number of pages17
ISBN (Print)9783662482872
Publication statusPublished - 2015
Externally publishedYes
Event22nd International Static Analysis Symposium, SAS 2015 - Saint-Malo, France
Duration: 2015 Sept 92015 Sept 11

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other22nd International Static Analysis Symposium, SAS 2015

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Explaining the effectiveness of small refinement heuristics in program verification with CEGAR'. Together they form a unique fingerprint.

Cite this