Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
CoRR(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要