In this work, we study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). LTL is a rich and expressive logic that can specify important properties of programs. This includes, but is not limited to, termination, safety, liveness, progress, recurrence and reach-avoid properties. We first present novel sound and complete witnesses for LTL verification over imperative programs. Our witnesses are applicable to both universal (all runs) and existential (some run) settings. We then consider polynomial arithmetic programs, i.e. programs in which every assignment and guard consists only of polynomial expressions, with specifications as LTL formulas in which atomic propositions are polynomial constraints. For this setting, we provide an efficient algorithm to automatically synthesize such LTL witnesses. Our synthesis procedure is both sound and semi-complete, i.e. complete for any fixed polynomial degree in the templates. In other words, we provide the first template-based approach for polynomial programs that can handle any LTL formula as its specification. Our approach has termination guarantees with sub-exponential time complexity and generalizes and unifies previous methods for termination, safety and reachability, since they are expressible in LTL. Finally, we present experimental results demonstrating the effectiveness of our approach and that it can handle programs which were beyond the reach of previous state-of-the-art tools.

翻译：本文研究了关于线性时序逻辑(LTL)形式规约的程序验证这一经典问题。LTL是一种丰富且具有表达力的逻辑，能够描述程序的重要性质，包括但不限于：终止性、安全性、活性、进展性、循环性以及可达-回避性质。我们首先提出了一种新颖的、用于命令式程序LTL验证的完备可靠见证。该见证方法同时适用于全称（所有运行）和存在（某些运行）两种设定。接着，我们考虑了多项式算术程序，即每个赋值语句和守卫条件均由多项式表达式构成的程序，其规约为原子命题是多项式约束的LTL公式。针对这一设定，我们提供了一种高效算法来自动合成此类LTL见证。该合成过程既可靠又半完备，即对模板中任意固定多项式次数而言是完备的。换言之，我们首次提出了能够处理任意LTL公式作为规约的多项式程序模板化方法。该方法具有次指数时间复杂度的终止保证，并推广统一了先前关于终止性、安全性和可达性的方法，因为这些性质均可由LTL表达。最后，我们通过实验验证了该方法的有效性，并展示了其能够处理先前最先进工具无法企及的程序。