We present the new version of 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 a novel calculus 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 SMT solving and unsat cores. An extensive evaluation shows that LoAT is highly competitive with other state-of-the-art tools for proving non-termination. While no other tool is able to deduce worst-case lower bounds for full integer programs, we also demonstrate that LoAT significantly outperforms its predecessors.
翻译：我们展示了新版本的循环加速工具(Loop 加速工具), 这是一种强有力的工具,用来证明不终止和对以整数操作的程序进行最坏的下限。 它基于循环加速的新微积分, 即将循环转换成非确定性直线代码, 并用于寻找非终止性配置。 为了高效地实施它, Loop 加速工具(Loop 加速工具) 采用了基于 SMT 解析和不观测核心的新方法。 一项广泛的评估显示, LoAT 与其他最先进的工具相比, 具有高度的竞争力, 可以证明不终止性。 虽然其他工具都无法为完全整数程序推断出最坏的下限, 但我们也证明LoAT 大大优于其前身。
相关内容
- Today (iOS and OS X): widgets for the Today view of Notification Center
- Share (iOS and OS X): post content to web services or share content with others
- Actions (iOS and OS X): app extensions to view or manipulate inside another app
- Photo Editing (iOS): edit a photo or video in Apple's Photos app with extensions from a third-party apps
- Finder Sync (OS X): remote file storage in the Finder with support for Finder content annotation
- Storage Provider (iOS): an interface between files inside an app and other apps on a user's device
- Custom Keyboard (iOS): system-wide alternative keyboards
Source: iOS 8 Extensions: Apple’s Plan for a Powerful App Ecosystem
微信扫码咨询专知VIP会员