Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)

被引：9

作者：

Frohn, Florian ^{[1
]}

Giesl, Juergen ^{[1
]}

机构：

[1] Rhein Westfal TH Aachen, LuFG Informat 2, Aachen, Germany

来源：

AUTOMATED REASONING, IJCAR 2022 | 2022年 / 13385卷

关键词：

D O I：

10.1007/978-3-031-10769-6_41

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We present the Loop Acceleration Tool (LoAT), a powerful tool for proving non-termination and worst-case lower bounds for programs operating on integers. It is based on the novel calculus from [10,11] for loop acceleration, i.e., transforming loops into non-deterministic straight-line code, and for finding non-terminating configurations. To implement it efficiently, LoAT uses a new approach based on unsat cores. We evaluate LoAT's power and performance by extensive experiments.

引用

页码：712 / 722

页数：11

共 11 条

[1] Proving non-termination
Gupta, Ashutosh K.
Henzinger, Thomas A.
Majumdar, Rupak
Rybalchenko, Andrey
Xu, Ru-Gang
ACM SIGPLAN NOTICES, 2008, 43 (01) : 147 - 158
[2] Proving Non-Termination
Gupta, Ashutosh K.
Henzinger, Thomas A.
Majumdar, Rupak
Rybalchenko, Andrey
Xu, Ru-Gang
POPL'08: PROCEEDINGS OF THE 35TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2008, : 147 - 158
[3] Non-termination Proving at Scale
Raad, Azalea
Vanegue, Julien
O'Hearn, Peter
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2024, 8 (OOPSLA):
[4] Proving Non-termination by Program Reversal
Chatterjee, Krishnendu
Goharshady, Ehsan Kafshdar
Novotny, Petr
Zikelic, Dorde
PROCEEDINGS OF THE 42ND ACM SIGPLAN INTERNATIONAL CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '21), 2021, : 1033 - 1048
[5] Proving Non-Termination via Loop Acceleration
Frohn, Florian
Gies, Juergen
2019 FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD), 2019, : 221 - 230
[6] Proving Non-termination Using Max-SMT
Larraz, Daniel
Nimkar, Kaustubh
Oliveras, Albert
Rodriguez-Carbonell, Enric
Rubio, Albert
COMPUTER AIDED VERIFICATION, CAV 2014, 2014, 8559 : 779 - 796
[7] Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper)
Frohn, Florian
Giesl, Juergen
AUTOMATED DEDUCTION, CADE 29, 2023, 14132 : 220 - 233
[8] Non-determinism, Non-termination and the Strong Normalization of System T
Aschieri, Federico
Zorzi, Margherita
TYPED LAMBDA CALCULI AND APPLICATIONS, TLCA 2013, 2013, 7941 : 31 - 47
[9] HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)
Dalmonte, Tiziano
Olivetti, Nicola
Pozzato, Gian Luca
AUTOMATED REASONING, PT II, 2020, 12167 : 378 - 387
[10] MAXIMUM-LIKELIHOOD AND LOWER BOUNDS IN SYSTEM-IDENTIFICATION WITH NON-GAUSSIAN INPUTS
SHALVI, O
WEINSTEIN, E
IEEE TRANSACTIONS ON INFORMATION THEORY, 1994, 40 (02) : 328 - 339

← 1 2 →