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

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

1 Citation (Scopus)

Abstract

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
PublisherSpringer Verlag
Pages128-144
Number of pages17
Volume9291
ISBN (Print)9783662482872
DOIs
Publication statusPublished - 2015
Externally publishedYes
Event22nd International Static Analysis Symposium, SAS 2015 - Saint-Malo, France
Duration: 2015 Sep 92015 Sep 11

Publication series

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

Other

Other22nd International Static Analysis Symposium, SAS 2015
CountryFrance
CitySaint-Malo
Period15/9/915/9/11

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint 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

    Terauchi, T. (2015). Explaining the effectiveness of small refinement heuristics in program verification with CEGAR. In Static Analysis- 22nd International Symposium, SAS 2015, Proceedings (Vol. 9291, pp. 128-144). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9291). Springer Verlag. https://doi.org/10.1007/978-3-662-48288-9_8