More Like this

1. Termination analysis without the tears

   https://doi.org/10.1145/3453483.3454110  

   Zhu, Shaowei ; Kincaid, Zachary ( June 2021 , Programming Language Design and Implementation)

   Determining whether a given program terminates is the quintessential undecidable problem. Algorithms for termination analysis may be classified into two groups: (1) algorithms with strong behavioral guarantees that work in limited circumstances (e.g., complete synthesis of linear ranking functions for polyhedral loops), and (2) algorithms that are widely applicable, but have weak behavioral guarantees (e.g., Terminator). This paper investigates the space in between: how can we design practical termination analyzers with useful behavioral guarantees? This paper presents a termination analysis that is both compositional (the result of analyzing a composite program is a function of the analysis results of its components) and monotone (“more information into the analysis yields more information out”). The paper has two key contributions. The first is an extension of Tarjan’s method for solving path problems in graphs to solve infinite path problems. This provides a foundation upon which to build compositional termination analyses. The second is a collection of monotone conditional termination analyses based on this framework. We demonstrate that our tool ComPACT (Compositional and Predictable Analysis for Conditional Termination) is competitive with state-of-the-art termination tools while providing stronger behavioral guarantees. 

   more » « less
2. Impact of Catalyzed Radical Termination (CRT) and Reductive Radical Termination (RRT) in Metal-Mediated Radical Polymerization Processes: Impact of Catalyzed Radical Termination (CRT) and Reductive Radical Termination (RRT) in Metal-Mediated Radical Polymerization Processes

   https://doi.org/10.1002/ejic.201900901  

   Thevenin, Lucas ; Fliedel, Christophe ; Matyjaszewski, Krzysztof ; Poli, Rinaldo ( October 2019 , European Journal of Inorganic Chemistry)
3. Reflections on Termination of Linear Loops

   https://doi.org/10.1007/978-3-030-81688-9_3  

   Zhu, Shaowei ; Kincaid, Zachary ( July 2021 , Computer Aided Verification)

   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. 

   more » « less
4. Almost-Sure Termination by Guarded Refinement

   https://doi.org/10.1145/3674632  

   Gregersen, Simon Oddershede ; Aguirre, Alejandro ; Haselwarter, Philipp G ; Tassarotti, Joseph ; Birkedal, Lars ( August 2024 , Proceedings of the ACM on Programming Languages)

   Almost-sure termination is an important correctness property for probabilistic programs, and a number of program logics have been developed for establishing it. However, these logics have mostly been developed for first-order programs written in languages with specific syntactic patterns for looping. In this paper, we consider almost-sure termination for higher-order probabilistic programs with general references. This combination of features allows for recursion and looping to be encoded through a variety of patterns. Therefore, rather than developing proof rules for reasoning about particular recursion patterns, we instead propose an approach based on proving refinement between a higher-order program and a simpler probabilistic model, in such a way that the refinement preserves termination behavior. By proving a refinement, almost-sure termination behavior of the program can then be established by analyzing the simpler model. We present this approach in the form of Caliper, a higher-order separation logic for proving termination-preserving refinements. Caliper uses probabilistic couplings to carry out relational reasoning between a program and a model. To handle the range of recursion patterns found in higher-order programs, Caliper uses guarded recursion, in particular the principle of Löb induction. A technical novelty is that Caliper does not require the use of transfinite step indexing or other technical restrictions found in prior work on guarded recursion for termination-preservation refinement. We demonstrate the flexibility of this approach by proving almost-sure termination of several examples, including first-order loop constructs, a random list generator, treaps, and a sampler for Galton-Watson trees that uses higher-order store. All the results have been mechanized in the Coq proof assistant. 

   more » « less
5. Robust to Early Termination Model Predictive Control

   https://doi.org/10.1109/TAC.2023.3308817  

   Hosseinzadeh, Mehdi ; Sinopoli, Bruno ; Kolmanovsky, Ilya ; Baruah, Sanjoy ( August 2023 , IEEE Transactions on Automatic Control)