Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

9-2024

Abstract

We study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). We first present novel sound and complete witnesses for LTL verification over imperative programs. Our witnesses are applicable to both verification (proving) and refutation (finding bugs) 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.

Discipline

Artificial Intelligence and Robotics | Programming Languages and Compilers

Research Areas

Intelligent Systems and Optimization

Areas of Excellence

Digital transformation

Publication

Proceedings of the 26th International Symposium, FM 2024, Milan, Italy, 2024 September 9-13

First Page

600

Last Page

619

ISBN

978303171161

Identifier

10.1007/978-3-031-71162-6_31

Publisher

Springer

City or Country

Cham

Additional URL

https://doi.org/10.1007/978-3-031-71162-6_31

Download

Share

COinS