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

research-article

Open access

Non-termination Proving at Scale

Authors:

Julien Vanegue,

Peter O’HearnAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 8, Issue OOPSLA2

Article No.: 280, Pages 246 - 274

https://doi.org/10.1145/3689720

Published: 08 October 2024 Publication History

Abstract

Program termination is a classic non-safety property whose falsification cannot in general be witnessed by a finite trace. This makes testing for non-termination challenging, and also a natural target for symbolic proof. Several works in the literature apply non-termination proving to small, self-contained benchmarks, but it has not been developed for large, real-world projects; as such, despite its allure, non-termination proving has had limited practical impact. We develop a compositional theory for non-termination proving, paving the way for its scalable application to large codebases. Discovering non-termination is an under-approximate problem, and we present UNTer, a sound and complete under-approximate logic for proving non-termination. We then extend UNTer with separation logic and develop UNTer^SL for heap-manipulating programs, yielding a compositional proof method amenable to automation via under-approximation and bi-abduction. We extend the Pulse analyser from Meta and develop Pulse^∞, an automated, compositional prover for non-termination based on UNTer^SL. We have run Pulse^∞ on large codebases and libraries, each comprising hundreds of thousands of lines of code, including OpenSSL, libxml2, libxpm and CryptoPP; it discovered several previously-unknown non-termination bugs and have reported them to developers of these libraries.

References

[1]

Krzysztof R. Apt and Ernst-Rüdiger Olderog. 2019. Fifty years of Hoare’s logic. Formal Aspects Comput., 31, 6 (2019), 751–807. https://doi.org/10.1007/s00165-019-00501-3

Digital Library

[2]

Flavio Ascari, Roberto Bruni, Roberta Gori, and Francesco Logozzo. 2024. Sufficient Incorrectness Logic: SIL and Separation SIL. arxiv:2310.18156. arxiv:2310.18156

[3]

Thomas Ball, Orna Kupferman, and Greta Yorsh. 2005. Abstraction for Falsification. In Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings, Kousha Etessami and Sriram K. Rajamani (Eds.) (Lecture Notes in Computer Science, Vol. 3576). Springer, 67–81. https://doi.org/10.1007/11513988_8

Digital Library

[4]

Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, and Peter O’Hearn. 2007. Variance Analyses from Invariance Analyses. SIGPLAN Not., 42, 1 (2007), jan, 211–224. issn:0362-1340 https://doi.org/10.1145/1190215.1190249

Digital Library

[5]

Josh Berdine, Byron Cook, Dino Distefano, and Peter W. O’Hearn. 2006. Automatic Termination Proofs for Programs with Shape-Shifting Heaps. In Computer Aided Verification, Thomas Ball and Robert B. Jones (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 386–400. isbn:978-3-540-37411-4

[6]

Sam Blackshear, Nikos Gorogiannis, Peter W. O’Hearn, and Ilya Sergey. 2018. RacerD: Compositional Static Race Detection. Proc. ACM Program. Lang., 2, OOPSLA (2018), Article 144, Oct., 28 pages. https://doi.org/10.1145/3276514

Digital Library

[7]

Marc Brockschmidt, Byron Cook, and Carsten Fuhs. 2013. Better termination proving through cooperation. In Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 25. 413–429.

[8]

James Brotherston and Nikos Gorogiannis. 2014. Cyclic Abduction of Inductively Defined Safety and Termination Preconditions. In Static Analysis, Markus Müller-Olm and Helmut Seidl (Eds.). Springer International Publishing, Cham. 68–84. isbn:978-3-319-10936-7

[9]

Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. 2011. Compositional Shape Analysis by Means of Bi-Abduction. J. ACM, 58, 6 (2011), Article 26, Dec., 66 pages. issn:0004-5411 http://doi.acm.org/10.1145/2049697.2049700

Digital Library

[10]

Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotnỳ, and Đ orđ e Žikelić. 2021. Proving non-termination by program reversal. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 1033–1048.

Digital Library

[11]

Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, and Hongseok Yang. 2008. Ranking Abstractions. In Programming Languages and Systems, Sophia Drossopoulou (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 148–162. isbn:978-3-540-78739-6

[12]

Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, and Peter W. O’Hearn. 2014. Proving Nontermination via Safety. In Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, Erika Ábrahám and Klaus Havelund (Eds.) (Lecture Notes in Computer Science, Vol. 8413). Springer, 156–171. https://doi.org/10.1007/978-3-642-54862-8_11

[13]

Byron Cook, Carsten Fuhs, Kaustubh Nimkar, and Peter W. O’Hearn. 2015. Embracing Overapproximation for Proving Nontermination. Tiny Trans. Comput. Sci., 3 (2015), http://tinytocs.org/vol3/papers/TinyToCS_3_cook.pdf

[14]

Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. Termination Proofs for Systems Code. SIGPLAN Not., 41, 6 (2006), jun, 415–426. issn:0362-1340 https://doi.org/10.1145/1133255.1134029

Digital Library

[15]

Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. Terminator: Beyond Safety. In Computer Aided Verification, Thomas Ball and Robert B. Jones (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 415–418. isbn:978-3-540-37411-4

[16]

Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2011. Proving program termination. Commun. ACM, 54, 5 (2011), 88–98. https://doi.org/10.1145/1941487.1941509

Digital Library

[17]

Byron Cook, Abigail See, and Florian Zuleger. 2013. Ramsey vs. lexicographic termination proving. In Tools and Algorithms for the Construction and Analysis of Systems: 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings 19. 47–61.

[18]

Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, and Julian Sutherland. 2016. Modular Termination Verification for Non-blocking Concurrency. In Programming Languages and Systems, Peter Thiemann (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 176–201. isbn:978-3-662-49498-1

[19]

Edsko de Vries and Vasileios Koutavas. 2011. Reverse Hoare Logic. In Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings. 155–171. https://doi.org/10.1007/978-3-642-24690-6_12

[20]

Dino Distefano, Manuel Fähndrich, Francesco Logozzo, and Peter W. O’Hearn. 2019. Scaling static analyses at Facebook. Commun. ACM, 62, 8 (2019), 62–70. https://doi.org/10.1145/3338112

Digital Library

[21]

Emanuele D’Osualdo, Julian Sutherland, Azadeh Farzan, and Philippa Gardner. 2021. TaDA Live: Compositional Reasoning for Termination of Fine-Grained Concurrent Programs. ACM Trans. Program. Lang. Syst., 43, 4 (2021), Article 16, nov, 134 pages. issn:0164-0925 https://doi.org/10.1145/3477082

Digital Library

[22]

Patrice Godefroid. 2005. The soundness of bugs is what matters (position statement). https://www.cs.umd.edu/~pugh/BugWorkshop05/papers/11-godefroid.pdf

[23]

Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, and SaiDeep Tetali. 2010. Compositional may-must program analysis: unleashing the power of alternation. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, Manuel V. Hermenegildo and Jens Palsberg (Eds.). ACM, 43–56. https://doi.org/10.1145/1706299.1706307

Digital Library

[24]

Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, and Ru-Gang Xu. 2008. Proving non-termination. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, George C. Necula and Philip Wadler (Eds.). ACM, 147–158. https://doi.org/10.1145/1328438.1328459

Digital Library

[25]

David Harel. 1979. First-Order Dynamic Logic. Springer-Verlag, Berlin, Heidelberg. isbn:0387092374

[26]

William R Harris, Akash Lal, Aditya V Nori, and Sriram K Rajamani. 2010. Alternation for termination. In Static Analysis: 17th International Symposium, SAS 2010, Perpignan, France, September 14-16, 2010. Proceedings 17. 304–319.

[27]

Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2014. Termination Analysis by Learning Terminating Programs. In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham. 797–813. isbn:978-3-319-08867-9

[28]

Jera Hensel, Constantin Mensendiek, and Jürgen Giesl. 2022. AProVE: Non-Termination Witnesses for C Programs: (Competition Contribution). In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 403–407.

Digital Library

[29]

Samin S. Ishtiaq and Peter W. O’Hearn. 2001. BI as an Assertion Language for Mutable Data Structures. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). Association for Computing Machinery, New York, NY, USA. 14–26. isbn:1581133367 https://doi.org/10.1145/360204.375719

Digital Library

[30]

Daniel Kroening, Natasha Sharygina, Aliaksei Tsitovich, and Christoph M Wintersteiger. 2010. Termination analysis with compositional transition invariants. In International Conference on Computer Aided Verification. 89–103.

Digital Library

[31]

Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell, and Albert Rubio. 2014. Proving non-termination using Max-SMT. In Computer Aided Verification: 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings 26. 779–796.

Digital Library

[32]

Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 2022. Finding Real Bugs in Big Programs with Incorrectness Logic. Proc. ACM Program. Lang., 6, OOPSLA1 (2022), Article 81, apr, 27 pages. https://doi.org/10.1145/3527325

Digital Library

[33]

Ton Chanh Le, Timos Antonopoulos, Parisa Fathololumi, Eric Koskinen, and ThanhVu Nguyen. 2020. DynamiTe: dynamic termination and non-termination proofs. Proc. ACM Program. Lang., 4, OOPSLA (2020), Article 189, nov, 30 pages. https://doi.org/10.1145/3428257

Digital Library

[34]

Ton Chanh Le, Cristian Gherghina, Aquinas Hobor, and Wei-Ngan Chin. 2014. A resource-based logic for termination and non-termination proofs. In Formal Methods and Software Engineering: 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, Luxembourg, November 3-5, 2014. Proceedings 16. 267–283.

[35]

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, Portland, OR, USA, June 15-17, 2015, David Grove and Stephen M. Blackburn (Eds.). ACM, 489–498. https://doi.org/10.1145/2737924.2737993

Digital Library

[36]

Hongjin Liang and Xinyu Feng. 2016. A Program Logic for Concurrent Objects under Fair Scheduling. SIGPLAN Not., 51, 1 (2016), jan, 385–399. issn:0362-1340 https://doi.org/10.1145/2914770.2837635

Digital Library

[37]

Bernhard Möller, Peter W. O’Hearn, and Tony Hoare. 2021. On Algebra of Program Correctness and Incorrectness. In Relational and Algebraic Methods in Computer Science - 19th International Conference, RAMiCS 2021, Marseille, France, November 2-5, 2021, Proceedings, Uli Fahrenberg, Mai Gehrke, Luigi Santocanale, and Michael Winter (Eds.) (Lecture Notes in Computer Science, Vol. 13027). Springer, 325–343. https://doi.org/10.1007/978-3-030-88701-8_20

Digital Library

[38]

Peter W. O’Hearn. 2019. Incorrectness Logic. Proc. ACM Program. Lang., 4, POPL (2019), Article 10, Dec., 32 pages. issn:2475-1421 http://doi.acm.org/10.1145/3371078

Digital Library

[39]

Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O’Hearn, and Jules Villard. 2020. Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. In Computer Aided Verification, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing, Cham. 225–252. isbn:978-3-030-53291-8

[40]

Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 2022. Concurrent Incorrectness Separation Logic. Proc. ACM Program. Lang., 6, POPL (2022), Article 34, jan, 29 pages. https://doi.org/10.1145/3498695

Digital Library

[41]

Azalea Raad, Julien Vanegue, Josh Berdine, and Peter O’Hearn. 2023. A General Approach to Under-Approximate Reasoning About Concurrent Programs. In 34th International Conference on Concurrency Theory (CONCUR 2023), Guillermo A. Pérez and Jean-François Raskin (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 279). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 25:1–25:17. isbn:978-3-95977-299-0 issn:1868-8969 https://doi.org/10.4230/LIPIcs.CONCUR.2023.25

[42]

Azalea Raad, Julien Vanegue, and Peter O’Hearn. 2024. Extended Version. https://www.soundandcomplete.org/papers/OOPSLA2024/Unter/

[43]

Azalea Raad, Julien Vanegue, and Peter O’Hearn. 2024. The Pulse ∞ prototype tool. https://doi.org/10.5281/zenodo.12637589

Digital Library

[44]

Caitlin Sadowski, Edward Aftandilian, Alex Eagle, Liam Miller-Cushon, and Ciera Jaspan. 2018. Lessons from Building Static Analysis Tools at Google. Commun. ACM, 61, 4 (2018), March, 58–66. issn:0001-0782 https://doi.org/10.1145/3188720

Digital Library

[45]

Xiuhan Shi, Xiaofei Xie, Yi Li, Yao Zhang, Sen Chen, and Xiaohong Li. 2022. Large-scale analysis of non-termination bugs in real-world OSS projects. In Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2022, Singapore, Singapore, November 14-18, 2022, Abhik Roychoudhury, Cristian Cadar, and Miryung Kim (Eds.). ACM, 256–268. https://doi.org/10.1145/3540250.3549129

Digital Library

[46]

Helga Velroyen and Philipp Rümmer. 2008. Non-termination checking for imperative programs. In International Conference on Tests and Proofs. 154–170.

[47]

Noam Zilberstein, Derek Dreyer, and Alexandra Silva. 2023. Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning. Proc. ACM Program. Lang., 7, OOPSLA1 (2023), Article 93, apr, 29 pages. https://doi.org/10.1145/3586045

Digital Library

[48]

Noam Zilberstein, Angelina Saliling, and Alexandra Silva. 2024. Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects. Proc. ACM Program. Lang., 8, OOPSLA1 (2024), Article 104, apr, 29 pages. https://doi.org/10.1145/3649821

Digital Library

Cited By

Zhang LZilberstein NKaminski BSilva A(2024)Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate TransformersProceedings of the ACM on Programming Languages10.1145/36897408:OOPSLA2(817-845)Online publication date: 8-Oct-2024
https://doi.org/10.1145/3689740
Zilberstein NSridharan M(2024)Unified Analysis Techniques for Programs with OutcomesCompanion Proceedings of the 2024 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity10.1145/3689491.3691814(4-6)Online publication date: 20-Oct-2024
https://dl.acm.org/doi/10.1145/3689491.3691814

Index Terms

Non-termination Proving at Scale
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
      2. Program verification

Recommendations

Proving non-termination
POPL '08

The search for proof and the search for counterexamples (bugs) are complementary activities that need to be pursued concurrently in order to maximize the practical success rate of verification tools.While this is well-understood in safety verification, ...
Proving non-termination
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

The search for proof and the search for counterexamples (bugs) are complementary activities that need to be pursued concurrently in order to maximize the practical success rate of verification tools.While this is well-understood in safety verification, ...
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties

Hoare logics are proof systems that allow one to formally establish properties of computer programs. Traditional Hoare logics prove properties of individual program executions (such as functional correctness). Hoare logic has been generalized to prove ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 8, Issue OOPSLA2

October 2024

2691 pages

EISSN:2475-1421

DOI:10.1145/3554319

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2024 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 October 2024

Published in PACMPL Volume 8, Issue OOPSLA2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

UKRI
EPSRC
NCSC

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
499
Total Downloads

Downloads (Last 12 months)499
Downloads (Last 6 weeks)151

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Zhang LZilberstein NKaminski BSilva A(2024)Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate TransformersProceedings of the ACM on Programming Languages10.1145/36897408:OOPSLA2(817-845)Online publication date: 8-Oct-2024
https://doi.org/10.1145/3689740
Zilberstein NSridharan M(2024)Unified Analysis Techniques for Programs with OutcomesCompanion Proceedings of the 2024 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity10.1145/3689491.3691814(4-6)Online publication date: 20-Oct-2024
https://dl.acm.org/doi/10.1145/3689491.3691814

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents