Syndicate: Synergistic Synthesis of Ranking Function and Invariants for Termination Analysis
CoRR(2024)
Abstract
Several techniques have been developed to prove the termination of programs.
Finding ranking functions is one of the common approaches to do so. A ranking
function must be bounded and must reduce at every iteration for all the
reachable program states. Since the set of reachable states is often unknown,
invariants serve as an over-approximation. Further, in the case of nested
loops, the initial set of program states for the nested loop can be determined
by the invariant of the outer loop. So, invariants play an important role in
proving the validity of a ranking function in the absence of the exact
reachable states. However, in the existing techniques, either the invariants
are synthesized independently, or combined with ranking function synthesis into
a single query, both of which are inefficient.
We observe that a guided search for invariants and ranking functions can have
benefits in terms of the number of programs that can be proved to terminate and
the time needed to identify a proof of termination. So, in this work, we
develop Syndicate, a novel framework that synergistically guides the search for
both the ranking function and an invariant that together constitute a proof of
termination. Owing to our synergistic approach, Syndicate can not only prove
the termination of more benchmarks but also achieves a reduction ranging from
17
termination analysis tools. We also prove that Syndicate is relatively
complete, i.e., if there exists a ranking function and an invariant in their
respective templates that can be used to prove the termination of a program,
then Syndicate will always find it if there exist complete procedures for the
template-specific functions in our framework.
MoreTranslated text
AI Read Science
Must-Reading Tree
Example
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined