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

Fingerprint

Program Verification
Refinement
Heuristics
Predicate
Counterexample
Computer programming languages
Turing
Reachability
Programming Languages
Safety
Iteration
Abstraction

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

Explaining the effectiveness of small refinement heuristics in program verification with CEGAR. / Terauchi, Tachio.

Static Analysis- 22nd International Symposium, SAS 2015, Proceedings. Vol. 9291 Springer Verlag, 2015. p. 128-144 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9291).

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

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, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9291, Springer Verlag, pp. 128-144, 22nd International Static Analysis Symposium, SAS 2015, Saint-Malo, France, 15/9/9. https://doi.org/10.1007/978-3-662-48288-9_8
Terauchi T. Explaining the effectiveness of small refinement heuristics in program verification with CEGAR. In Static Analysis- 22nd International Symposium, SAS 2015, Proceedings. Vol. 9291. Springer Verlag. 2015. p. 128-144. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-662-48288-9_8
Terauchi, Tachio. / Explaining the effectiveness of small refinement heuristics in program verification with CEGAR. Static Analysis- 22nd International Symposium, SAS 2015, Proceedings. Vol. 9291 Springer Verlag, 2015. pp. 128-144 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{880dbe51df214d31985a361da264ecf4,
title = "Explaining the effectiveness of small refinement heuristics in program verification with CEGAR",
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.",
author = "Tachio Terauchi",
year = "2015",
doi = "10.1007/978-3-662-48288-9_8",
language = "English",
isbn = "9783662482872",
volume = "9291",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "128--144",
booktitle = "Static Analysis- 22nd International Symposium, SAS 2015, Proceedings",
address = "Germany",

}

TY - GEN

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

AU - Terauchi, Tachio

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84946090522&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84946090522&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-48288-9_8

DO - 10.1007/978-3-662-48288-9_8

M3 - Conference contribution

SN - 9783662482872

VL - 9291

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 128

EP - 144

BT - Static Analysis- 22nd International Symposium, SAS 2015, Proceedings

PB - Springer Verlag

ER -