Synthesizing ranking functions is a typical technique for proving loop termination. In this work, we propose an approach to handle the backward, or the reverse, problem. That is, one constructs loops such that a given linear function is a ranking function for these loops. To achieve this, we firstly demonstrate by experiments the necessity to introduce parameters to increase the success ratio. We then formulate this problem as a proper existential quantifier elimination (or parametric system solving) problem, and propose two efficient methods to handle it. We have implemented our methods and demonstrated their effectiveness by extensive experiments.

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

Synthesizing Loops from Linear Ranking Functions

  • Rui-Juan Jing,
  • Yaru Yuan,
  • Yuxing Cai,
  • Yi Li,
  • Changbo Chen

摘要

Synthesizing ranking functions is a typical technique for proving loop termination. In this work, we propose an approach to handle the backward, or the reverse, problem. That is, one constructs loops such that a given linear function is a ranking function for these loops. To achieve this, we firstly demonstrate by experiments the necessity to introduce parameters to increase the success ratio. We then formulate this problem as a proper existential quantifier elimination (or parametric system solving) problem, and propose two efficient methods to handle it. We have implemented our methods and demonstrated their effectiveness by extensive experiments.