Reflections on Termination of Linear Loops

Shaowei Zhu, Zachary Kincaid

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

1 Scopus citations


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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 33rd International Conference, CAV 2021, Proceedings
EditorsAlexandra Silva, K. Rustan Leino
PublisherSpringer Science and Business Media Deutschland GmbH
Number of pages24
ISBN (Print)9783030816872
StatePublished - 2021
Event33rd International Conference on Computer Aided Verification, CAV 2021 - Virtual, Online
Duration: Jul 20 2021Jul 23 2021

Publication series

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


Conference33rd International Conference on Computer Aided Verification, CAV 2021
CityVirtual, Online

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


  • Best abstraction
  • Conditional termination
  • Linear dynamical systems
  • Monotone analysis
  • Reflective subcategory
  • Termination


Dive into the research topics of 'Reflections on Termination of Linear Loops'. Together they form a unique fingerprint.

Cite this