Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs

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.