Many decision problems, particularly those concerning program semantics, are undecidable. One prominent example is determining whether a program terminates. To address this, modern static analyzers employ heuristics to prove termination, which could be effective for certain programs but not all. Users of these analyzers struggle to understand why the tool works or not for their source programs, due to the unpredictable behavior of heuristics. For instance, annotating a loop with an invariant might make a tool that previously worked fail or not terminate.

This dissertation investigates methodologies for designing termination analyses that can prove termination of real-world programs while ensuring predictability through monotonicity. A monotone analysis maintains or improves its results with additional input information, such as more loop invariants or assumptions that limit the program's state space. Monotonicity aligns with user expectations that analysis results should not deteriorate with more information given to the analysis.

To achieve a monotone program analysis, we extend the algebraic program analysis framework, which uses regular expressions to represent finite program paths and interpret labels and operators within these expressions. We introduce a framework for compositional and monotone termination analysis on whole programs by incorporating an omega operator to represent infinite paths, and we develop various monotone termination analyses through different implementations of this operator based on various techniques, including analyzing phase transitions in loops, abstracting the behavior of the loop into a linear dynamical system, or synthesizing (lexicographic) polynomials ranking functions. 

Experimental results demonstrate that it is possible to design monotone static termination analysis that is effective for both linear and nonlinear programs and competitive with the state-of-the-art non-monotone methods in terms of the number of benchmark tasks solved and running time.