@inproceedings{7c80cd1dc8ea4ee29e371b817a704501,
title = "Reflections on Termination of Linear Loops",
abstract = "This paper shows how techniques for linear dynamical systems can be used to reason about the behavior of general loops. We present two main results. First, we show that every loop that can be expressed as a transition formula in linear integer arithmetic has a best model as a deterministic affine transition system. Second, we show that for any linear dynamical system f with integer eigenvalues and any integer arithmetic formula G, there is a linear integer arithmetic formula that holds exactly for the states of f for which G is eventually invariant. Combining the two, we develop a monotone conditional termination analysis for general loops.",
keywords = "Best abstraction, Conditional termination, Linear dynamical systems, Monotone analysis, Reflective subcategory, Termination",
author = "Shaowei Zhu and Zachary Kincaid",
note = "Funding Information: Acknowledgments. This work was supported in part by the NSF under grant number 1942537 and by ONR under grant N00014-19-1-2318. Opinions, findings, conclusions, or recommendations expressed herein are those of the authors and do not necessarily reflect the views of the sponsoring agencies. Publisher Copyright: {\textcopyright} 2021, The Author(s).; 33rd International Conference on Computer Aided Verification, CAV 2021 ; Conference date: 20-07-2021 Through 23-07-2021",
year = "2021",
doi = "10.1007/978-3-030-81688-9_3",
language = "English (US)",
isbn = "9783030816872",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "51--74",
editor = "Alexandra Silva and Leino, {K. Rustan}",
booktitle = "Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings",
address = "Germany",
}