We study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). We first present novel \emph{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 LTL formulas in which atomic propositions can be polynomial constraints and turn our focus to polynomial arithmetic programs, i.e. programs in which every assignment and guard consists only of polynomial expressions. For this setting, we provide an efficient algorithm to automatically synthesize such LTL witnesses. Our synthesis procedure is both sound and semi-complete. 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见证，该综合过程兼具可靠性与半完备性。最后通过实验证明，本方法能有效处理超出先前最先进工具能力范围的程序。