Synthesizing ranking functions is a common technique for proving the termination of loops. A ranking function must be bounded and decrease by a specified amount with each iteration for all reachable program states. Since the set of reachable states is unknown, loop invariants are used to over-approximate it, requiring the joint synthesis of ranking functions and invariants. Existing approaches either synthesize them independently, encode them into a single monolithic query, or connect them through ad hoc, one-way information flow, leading to inefficient exploration of large search spaces. We present Syndicate, a termination analysis framework based on the novel concept of Bidirectional Decompositional Search (BDS). BDS keeps the ranking function and invariant synthesis decomposed but ensures continuous bi-directional feedback. This mutual guidance enables efficient exploration, significantly increasing the number of programs proven to terminate while reducing runtime compared to baselines without such feedback. Depending on the templates used, Syndicate is both relatively complete and provably efficient, outperforming existing techniques that achieve at most one of these guarantees. Despite its simplicity, Syndicate matches or surpasses state-of-the-art tools in termination proofs and runtime, demonstrating the effectiveness of bi-directional reasoning in termination analysis. Github: https://github.com/uiuc-focal-lab/Syndicate

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Efficient Ranking Function-Based Termination Analysis via Bidirectional Decompositional Search

  • Yasmin Chandini Sarita,
  • Avaljot Singh,
  • Shaurya Gomber,
  • Gagandeep Singh,
  • Mahesh Vishwanathan

摘要

Synthesizing ranking functions is a common technique for proving the termination of loops. A ranking function must be bounded and decrease by a specified amount with each iteration for all reachable program states. Since the set of reachable states is unknown, loop invariants are used to over-approximate it, requiring the joint synthesis of ranking functions and invariants. Existing approaches either synthesize them independently, encode them into a single monolithic query, or connect them through ad hoc, one-way information flow, leading to inefficient exploration of large search spaces. We present Syndicate, a termination analysis framework based on the novel concept of Bidirectional Decompositional Search (BDS). BDS keeps the ranking function and invariant synthesis decomposed but ensures continuous bi-directional feedback. This mutual guidance enables efficient exploration, significantly increasing the number of programs proven to terminate while reducing runtime compared to baselines without such feedback. Depending on the templates used, Syndicate is both relatively complete and provably efficient, outperforming existing techniques that achieve at most one of these guarantees. Despite its simplicity, Syndicate matches or surpasses state-of-the-art tools in termination proofs and runtime, demonstrating the effectiveness of bi-directional reasoning in termination analysis. Github: https://github.com/uiuc-focal-lab/Syndicate