| Summary: | Termination proof synthesis for simple loops, i.e., loops with only conjoined constraints in
the loop guard and variable updates in the loop body, is the building block of termination
analysis, as well as liveness analysis, for large complex imperative systems. In particular,
we consider a subclass of simple loops which contain only linear constraints in the loop
guard and linear updates in the loop body. We call them Linear Simple Loops (LSLs).
LSLs are particularly interesting because most loops in practice are indeed linear; more
importantly, since we allow the update statements to handle nondeterminism, LSLs are
expressive enough to serve as a foundational model for non-linear loops as well. Existing
techniques can successfully synthesize a linear ranking function for an LSL if there exists
one. When a terminating LSL does not have a linear ranking function, these techniques fail.
In this dissertation we describe an automatic method that generates proofs of (universal)
termination for LSLs based on the synthesis of disjunctive ranking relations. The method
repeatedly finds linear ranking functions on parts of the state space and checks whether the
transitive closure of the transition relation is included in the union of the ranking relations.
We have implemented the method and have shown experimental evidence of the effectiveness
of our method.
|
|---|
