Committee

  • Zak Kincaid (advisor)
  • Aarti Gupta
  • Andrew Appel

Title

A compositional and monotone approach to conditional termination of programs

Abstract

Modern reactive systems such as operating systems, servers, mobile applications, and even Ethereum-based smart contracts consist of software components whose executions are expected to terminate. Non-terminating executions result in unresponsiveness and might lead to other undesirable behaviors. Proving termination of program components, even though undecidable in general, is thus essential to ensure software reliability and remains an active area of research (e.g., Terminator, AProVE, Ultimate Automizer). However, existing tools suffer from unpredictability when run on real-world programs. The unpredictability results from the heuristic choices these tools make during the reasoning process. To address this issue, we describe a new conditional termination analysis with distinguishing features of being compositional and predictable.

Our analysis is compositional in that we analyze each loop in isolation, and compute an under-approximation of the pre-condition under which this loop is guaranteed to terminate. In particular, we model the behavior of the loop using linear dynamical systems and analyze the asymptotic behavior of the dynamical system to synthesize sufficient conditions that guarantee termination. Our analysis is predictable in that (i) its termination is guaranteed; (ii) it produces anti-tone conditions, i.e., for formulas F entails G where F and G both represent transition systems, the terminating conditions it generates for F is weaker than that for G. We demonstrate that our approach can solve nearly as many benchmarks in the numerical subset of SV-COMP termination category as state-of-the-art termination tools, and is generally faster in terms of performance.

Reading List

Papers

Termination Related

Transition invariants for termination

  • B. Cook, A. Podelski, and A. Rybalchenko, “Abstraction Refinement for Termination.,” SAS, 2005.

Ranking function synthesis

  • Gonnord, Laure, David Monniaux, and Gabriel Radanne. "Synthesis of ranking functions using extremal counterexamples." ACM SIGPLAN Notices 50.6 (2015): 608-618.

Conditional termination

  • M. Bozga, R. Iosif, and F. Konecný, “Deciding Conditional Termination.” TACAS, 2012.

Reasoning about termination of linear loops using matrix exponentiation

  • A. Tiwari, “Termination of Linear Programs.” CAV, 2004.

Compositional Recurrence Analysis

  • A. Farzan and Z. Kincaid, “Compositional Recurrence Analysis,” FMCAD, 2015.

Software Model Checking and Program Analysis in General

  • Jhala, Ranjit, and Rupak Majumdar. "Software model checking." ACM Computing Surveys (CSUR) 41.4 (2009): 1-54.
  • Calcagno, Cristiano, et al. "Compositional shape analysis by means of bi-abduction." POPL 2009.
  • McMillan, Kenneth L. "Lazy abstraction with interpolants." International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg, 2006.
  • Tarjan, Robert Endre. "A unified approach to path problems." Journal of the ACM (JACM) 28.3 (1981): 577-593.

Textbooks

  • Bradley, Aaron R., and Zohar Manna. The calculus of computation: decision procedures with applications to verification. Springer Science & Business Media, 2007.
  • Nielson, Flemming, Hanne R. Nielson, and Chris Hankin. Principles of program analysis. Springer, 2015. [Chapter 4. Abstract Interpretation]
  • Pierce, Benjamin C., Types and programming languages. MIT press, 2002.

Slides

They can be found here in PDF format.

Questions

(including follow-up questions)
  1. Write down syntax and tying rules for simply-typed lambda calculus. Type check a simple expression. What does it mean for a type system to be sound?
  2. Write down some numerical abstract domains (e.g., sign, interval, octagonal relations, polyhedron, convex polyhedron, affine equations, etc). Do they have best abstract transformer? Why?
  3. What is an interpolant? How does MacMillan’s paper use interpolant? What’s the difference between interpolants and invariants? What does “lazy” mean in the title of this paper? Compare and contrast lazy interpolants, predicate abstraction, and abstract interpretation.
  4. Prove that terminating programs have ranking functions. To simplify, prove that terminating deterministic programs have ranking functions.
  5. Write out the context-free grammar for regular expressions and omega-regular expressions. Inductively define the set of strings recognized by any regular expression or omega-regular expression.