Article

Abstraction refinement for termination

Authors:

Andreas Podelski,

Andrey RybalchenkoAuthors Info & Claims

SAS'05: Proceedings of the 12th international conference on Static Analysis

Pages 87 - 101

https://doi.org/10.1007/11547662_8

Published: 07 September 2005 Publication History

Abstract

Abstraction can often lead to spurious counterexamples. Counterexample-guided abstraction refinement is a method of strengthening abstractions based on the analysis of these spurious counterexamples. For invariance properties, a counterexample is a finite trace that violates the invariant; it is spurious if it is possible in the abstraction but not in the original system. When proving termination or other liveness properties of infinite-state systems, a useful notion of spurious counterexamples has remained an open problem. For this reason, no counterexample-guided abstraction refinement algorithm was known for termination. In this paper, we address this problem and present the first known automatic counterexample-guided abstraction refinement algorithm for termination proofs. We exploit recent results on transition invariants and transition predicate abstraction. We identify two reasons for spuriousness: abstractions that are too coarse, and candidate transition invariants that are too strong. Our counterexample-guided abstraction refinement algorithm successively weakens candidate transition invariants and refines the abstraction.

References

[1]

I. Balaban, A. Pnueli, and L. D. Zuck. Shape analysis by predicate abstraction. In VMCAI'2005: Verification, Model Checking, and Abstract Interpretation, volume 3385 of LNCS, pages 164-180. Springer, 2005.

Digital Library

[2]

T. Ball, B. Cook, V. Levin, and S. K. Rajamani. SLAM and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. In IFM'2004: Fourth International Conference on Integrated Formal Methods, volume 2999 of LNCS, pages 1-20. Springer, 2004.

[3]

A. Biere, C. Artho, and V. Schuppan. Liveness checking as safety checking. In FMICS'02: Formal Methods for Industrial Critical Systems, volume 66(2) of ENTCS, 2002.

[4]

A. Bradley, Z. Manna, and H. Sipma. Termination of polynomial programs. In VMCAI'2005: Verification, Model Checking, and Abstract Interpretation, volume 3385 of LNCS. Springer, 2005.

Digital Library

[5]

S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in C. In ICSE'2003: Int. Conf. on Software Engineering, pages 385-395, 2003.

Digital Library

[6]

E. Clarke, O. Grumberg, and D. Peled. Model checking. MIT Press, December 1999.

Digital Library

[7]

M. Colón and H. Sipma. Synthesis of linear ranking functions. In TACAS'2001: Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of LNCS, pages 67-81. Springer, 2001.

Digital Library

[8]

M. Colón and H. Sipma. Practical methods for proving program termination. In CAV'2002: Computer Aided Verification, volume 2404 of LNCS, pages 442-454. Springer, 2002.

Digital Library

[9]

P. Cousot. Partial completeness of abstract fixpoint checking. In SARA'2000: Abstraction, Reformulation, and Approximation, volume 1864 of LNCS, pages 1-15. Springer, 2000.

Digital Library

[10]

P. Cousot. Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In VMCAI'2005: Verification, Model Checking, and Abstract Interpretation, volume 3385 of LNCS, pages 1-24. Springer, 2005.

Digital Library

[11]

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL'1977: Principles of Programming Languages, pages 238-252. ACM Press, 1977.

Digital Library

[12]

P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In POPL'1978: Principles of Programming Languages, pages 84-97. ACM Press, 1978.

Digital Library

[13]

S. Das and D. L. Dill. Successive approximation of abstract transition relations. In LICS'2001: Logic in Computer Science, pages 51-60. IEEE, 2001.

Digital Library

[14]

J. Hatcliff and M. B. Dwyer. Using the Bandera tool set to model-check properties of concurrent Java software. In CONCUR'2001: Concurrency Theory, volume 2154 of LNCS, pages 39-58. Springer, 2001.

Digital Library

[15]

T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In POPL'2004: Principles of Programming Languages, pages 232-244. ACM Press, 2004.

Digital Library

[16]

F. Ivancic, H. Jain, A. Gupta, and M. K. Ganai. Localization and register sharing for predicate abstraction. In TACAS'2005: Tools and Algorithms for Construction and Analysis of Systems, LNCS. Springer, 2005. To appear.

Digital Library

[17]

Y. Lakhnech, S. Bensalem, S. Berezin, and S. Owre. Incremental verification by abstraction. In TACAS'2001: Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of LNCS, pages 98-112. Springer, 2001.

Digital Library

[18]

Z. Manna and A. Pnueli. Temporal verification of reactive systems: Safety. Springer, 1995.

Digital Library

[19]

K. S. Namjoshi and R. P. Kurshan. Syntactic program transformations for automatic abstraction. In CAV'2000: Computer Aided Verification, volume 1855 of LNCS, pages 139-153. Springer, 2000.

Digital Library

[20]

A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI'2004: Verification, Model Checking, and Abstract Interpretation, volume 2937 of LNCS, pages 239-251. Springer, 2004.

[21]

A. Podelski and A. Rybalchenko. Transition invariants. In LICS'2004: Logic in Computer Science, pages 32-41. IEEE, 2004.

Digital Library

[22]

A. Podelski and A. Rybalchenko. Transition predicate abstraction and fair termination. In POPL'2005: Principles of Programming Languages, pages 132-144. ACM Press, 2005.

Digital Library

[23]

A. Podelski, I. Schaefer, and S. Wagner. Summaries for while programs with recursion. In S. Sagiv, editor, ESOP'2005: European Symposium on Programming, volume 3444 of LNCS, pages 94-107. Springer, 2005.

Digital Library

[24]

A. Tiwari. Termination of linear programs. In CAV'2004: Computer Aided Verification, volume 3114 of LNCS, pages 70-82. Springer, 2004.

Cited By

McMillan K(2024)Toward Liveness Proofs at ScaleComputer Aided Verification10.1007/978-3-031-65627-9_13(255-276)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65627-9_13
Smith CHsu JAlbarghouthi A(2019)Trace abstraction modulo probabilityProceedings of the ACM on Programming Languages10.1145/32903523:POPL(1-31)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290352
Ströder TGiesl JBrockschmidt MFrohn FFuhs CHensel JSchneider-Kamp PAschermann C(2017)Automatically Proving Termination and Memory Safety for Programs with Pointer ArithmeticJournal of Automated Reasoning10.1007/s10817-016-9389-x58:1(33-65)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1007/s10817-016-9389-x
Show More Cited By

Abstraction refinement for termination
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
2. Theory of computation

Recommendations

Transition predicate abstraction and fair termination
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Transition predicate abstraction and fair termination
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Transition predicate abstraction and fair termination
Special issue on POPL 2005

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

SAS'05: Proceedings of the 12th international conference on Static Analysis

September 2005

368 pages

ISBN:3540285849

Editors:
Chris Hankin
Department of Computing, Imperial College London
,
Igor Siveroni
Department of Computing, Imperial College London, 180 Queen's Gate, London, UK

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 07 September 2005

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

51
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 30 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

McMillan K(2024)Toward Liveness Proofs at ScaleComputer Aided Verification10.1007/978-3-031-65627-9_13(255-276)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65627-9_13
Smith CHsu JAlbarghouthi A(2019)Trace abstraction modulo probabilityProceedings of the ACM on Programming Languages10.1145/32903523:POPL(1-31)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290352
Ströder TGiesl JBrockschmidt MFrohn FFuhs CHensel JSchneider-Kamp PAschermann C(2017)Automatically Proving Termination and Memory Safety for Programs with Pointer ArithmeticJournal of Automated Reasoning10.1007/s10817-016-9389-x58:1(33-65)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1007/s10817-016-9389-x
Farzan AKincaid ZPodelski AKoskinen EGrohe MShankar N(2016)Proving Liveness of Parameterized ProgramsProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/2933575.2935310(185-196)Online publication date: 5-Jul-2016
https://dl.acm.org/doi/10.1145/2933575.2935310
Le TQin SChin W(2015)Termination and non-termination specification inferenceACM SIGPLAN Notices10.1145/2813885.273799350:6(489-498)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2813885.2737993
Le TQin SChin WGrove DBlackburn S(2015)Termination and non-termination specification inferenceProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2737924.2737993(489-498)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2737924.2737993
Kuwahara TTerauchi TUnno HKobayashi N(2014)Automatic Termination Verification for Higher-Order Functional ProgramsProceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 841010.1007/978-3-642-54833-8_21(392-411)Online publication date: 5-Apr-2014
https://dl.acm.org/doi/10.1007/978-3-642-54833-8_21
Massé D(2014)Policy Iteration-Based Conditional Termination and Ranking FunctionsProceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 831810.1007/978-3-642-54013-4_25(453-471)Online publication date: 19-Jan-2014
https://dl.acm.org/doi/10.1007/978-3-642-54013-4_25
Ganty PGenaim S(2013)Proving Termination Starting from the EndProceedings of the 25th International Conference on Computer Aided Verification - Volume 804410.5555/2958031.2958105(397-412)Online publication date: 13-Jul-2013
https://dl.acm.org/doi/10.5555/2958031.2958105
Cerny PHenzinger TRadhakrishna A(2013)Quantitative abstraction refinementACM SIGPLAN Notices10.1145/2480359.242908548:1(115-128)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2480359.2429085
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents