More Web Proxy on the site http://driver.im/

research-article

Proving termination by k-induction

Authors:

Fei HeAuthors Info & Claims

ASE '20: Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering

Pages 1239 - 1243

https://doi.org/10.1145/3324884.3418929

Published: 27 January 2021 Publication History

Abstract

We propose a novel approach to proving the termination of imperative programs by k-induction. By our approach, the termination proving problem can be formalized as a k-inductive invariant synthesis task. On the one hand, k-induction uses weaker invariants than that required by the standard inductive approach. On the other hand, the base case of k-induction, which unrolls the program, can provide stronger pre-condition for invariant synthesis. As a result, the termination arguments of our approach can be synthesized more efficiently than the standard method. We implement a prototype of our k-inductive approach. The experimental results show the significant effectiveness and efficiency of our approach.

References

[1]

Amir M Ben-Amram and Samir Genaim. 2013. On the linear ranking problem for integer linear-constraint loops. ACM SIGPLAN Notices 48, 1 (2013), 51--62.

Digital Library

[2]

Aaron R Bradley, Zohar Manna, and Henny B Sipma. 2005. Termination analysis of integer linear loops. In International Conference on Concurrency Theory. Springer, 488--502.

Digital Library

[3]

Martin Brain, Saurabh Joshi, Daniel Kroening, and Peter Schrammel. 2015. Safety verification and refutation by k-invariants and k-induction. In International Static Analysis Symposium. Springer, 145--161.

[4]

Michael A Colón, Sriram Sankaranarayanan, and Henny B Sipma. 2003. Linear invariant generation using non-linear constraint solving. In International Conference on Computer Aided Verification. Springer, 420--432.

[5]

Michael A Colóon and Henny B Sipma. 2001. Synthesis of linear ranking functions. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 67--81.

[6]

Leonardo De Moura, Harald Rueß, and Maria Sorea. 2003. Bounded model checking and induction: From refutation to verification. In International Conference on Computer Aided Verification. Springer, 14--26.

[7]

Alastair F Donaldson, Leopold Haller, Daniel Kroening, and Philipp Rümmer. 2011. Software verification using k-induction. In International Static Analysis Symposium. Springer, 351--368.

[8]

Grigory Fedyukovich, Samuel J Kaufman, and Rastislav Bodík. 2017. Sampling invariants from frequency distributions. In 2017 Formal Methods in Computer Aided Design (FMCAD). IEEE, 100--107.

[9]

Grigory Fedyukovich, Yueling Zhang, and Aarti Gupta. 2018. Syntax-guided termination analysis. In International Conference on Computer Aided Verification. Springer, 124--143.

[10]

Mikhail YR Gadelha, Hussama I Ismail, and Lucas C Cordeiro. 2017. Handling loops in bounded model checking of C programs via k-induction. International Journal on Software Tools for Technology Transfer 19, 1 (2017), 97--114.

Digital Library

[11]

Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, et al. 2014. Proving termination of programs automatically with AProVE. In International Joint Conference on Automated Reasoning. Springer, 184--191.

[12]

Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2014. Termination analysis by learning terminating programs. In International Conference on Computer Aided Verification. Springer, 797--813.

Digital Library

[13]

Kryštof Hoder and Nikolaj Bjørner. 2012. Generalized property directed reachability. In International Conference on Theory and Applications of Satisfiability Testing. Springer, 157--171.

Digital Library

[14]

Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. 2016. SMT-based model checking for recursive programs. Formal Methods in System Design 48, 3 (2016), 175--205.

Digital Library

[15]

Ton Chanh Le, Shengchao Qin, and Wei-Ngan Chin. 2015. Termination and non-termination specification inference. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. 489--498.

Digital Library

[16]

Jan Leike and Matthias Heizmann. 2014. Ranking templates for linear loops. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 172--186.

[17]

Andreas Podelski and Andrey Rybalchenko. 2004. A complete method for the synthesis of linear ranking functions. In International Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, 239--251.

[18]

Caterina Urban, Arie Gurfinkel, and Temesghen Kahsai. 2016. Synthesizing ranking functions from bits and pieces. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 54--70.

Digital Library

Cited By

Shi XXie XLi YZhang YChen SLi XRoychoudhury ACadar CKim M(2022)Large-scale analysis of non-termination bugs in real-world OSS projectsProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3540250.3549129(256-268)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3540250.3549129

Index Terms

Proving termination by k-induction
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
2. Theory of computation
  1. Logic
    1. Logic and verification

Recommendations

Proving termination properties with MU-TERM
AMAST'10: Proceedings of the 13th international conference on Algebraic methodology and software technology

MU-TERM is a tool which can be used to verify a number of termination properties of (variants of) Term Rewriting Systems (TRSs): termination of rewriting, termination of innermost rewriting, termination of order-sorted rewriting, termination of context-...
Proving termination of (conditional) rewrite systems

In this paper an important problem in the domain of term rewriting, the termination of (conditional) rewrite systems, is dealt with. We show that in many applications, well-founded orderings on terms which only make use of syntactic information of a ...
Proving termination of context-sensitive rewriting by transformation

Context-sensitive rewriting (CSR) is a restriction of rewriting that forbids reductions on selected arguments of functions. With CSR, we can achieve a terminating behavior with non-terminating term rewriting systems, by pruning (all) infinite rewrite ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASE '20: Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering

December 2020

1449 pages

ISBN:9781450367684

DOI:10.1145/3324884

General Chair:
John Grundy,
Program Chairs:
Claire Le Goues,
David Lo

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

In-Cooperation

IEEE CS

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 January 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

the Guangdong Science and Technology Department
the National Key R&D Program of China
the NSF of China

Conference

ASE '20

Sponsor:

ASE '20: 35th IEEE/ACM International Conference on Automated Software Engineering

December 21 - 25, 2020

Virtual Event, Australia

Acceptance Rates

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
75
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)1

Reflects downloads up to 22 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Shi XXie XLi YZhang YChen SLi XRoychoudhury ACadar CKim M(2022)Large-scale analysis of non-termination bugs in real-world OSS projectsProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3540250.3549129(256-268)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3540250.3549129

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents