Relaxed stratification

A new approach to practical complete predicate refinement

Tachio Terauchi, Hiroshi Unno

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

1 Citation (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationProgramming 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
PublisherSpringer Verlag
Pages610-633
Number of pages24
Volume9032
ISBN (Electronic)9783662466681
DOIs
Publication statusPublished - 2015
Externally publishedYes
Event24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 - London, United Kingdom
Duration: 2015 Apr 112015 Apr 18

Publication series

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

Other

Other24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
CountryUnited Kingdom
CityLondon
Period15/4/1115/4/18

Fingerprint

Stratification
Predicate
Refinement
Counterexample
Surface mount technology
Requirements
Interpolants
Reasoning
Language
Prototype
Sufficient
Restriction
Partial
Closed

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Terauchi, T., & Unno, H. (2015). Relaxed stratification: A new approach to practical complete predicate refinement. In 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 (Vol. 9032, pp. 610-633). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9032). Springer Verlag. https://doi.org/10.1007/978-3-662-46669-8_25

Relaxed stratification : A new approach to practical complete predicate refinement. / Terauchi, Tachio; Unno, Hiroshi.

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. Vol. 9032 Springer Verlag, 2015. p. 610-633 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9032).

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

Terauchi, T & Unno, H 2015, Relaxed stratification: A new approach to practical complete predicate refinement. in 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. vol. 9032, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9032, Springer Verlag, pp. 610-633, 24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, United Kingdom, 15/4/11. https://doi.org/10.1007/978-3-662-46669-8_25
Terauchi T, Unno H. Relaxed stratification: A new approach to practical complete predicate refinement. In 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. Vol. 9032. Springer Verlag. 2015. p. 610-633. (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-46669-8_25
Terauchi, Tachio ; Unno, Hiroshi. / Relaxed stratification : A new approach to practical complete predicate refinement. 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. Vol. 9032 Springer Verlag, 2015. pp. 610-633 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{84383d95d037465ea60fc6dc758bba91,
title = "Relaxed stratification: A new approach to practical complete predicate refinement",
abstract = "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.",
author = "Tachio Terauchi and Hiroshi Unno",
year = "2015",
doi = "10.1007/978-3-662-46669-8_25",
language = "English",
volume = "9032",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "610--633",
booktitle = "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",
address = "Germany",

}

TY - GEN

T1 - Relaxed stratification

T2 - A new approach to practical complete predicate refinement

AU - Terauchi, Tachio

AU - Unno, Hiroshi

PY - 2015

Y1 - 2015

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

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

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

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

U2 - 10.1007/978-3-662-46669-8_25

DO - 10.1007/978-3-662-46669-8_25

M3 - Conference contribution

VL - 9032

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

SP - 610

EP - 633

BT - 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

PB - Springer Verlag

ER -