Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs operating on integers. To this end, a variety of acceleration techniques has been proposed. However, all of them are monolithic: Either they accelerate a loop successfully, or they fail completely. In contrast, we present a calculus that allows for combining acceleration techniques in a modular way and we show how to integrate many existing acceleration techniques into our calculus. Moreover, we propose two novel acceleration techniques that can be incorporated into our calculus seamlessly. Some of these acceleration techniques apply only to non-terminating loops. Thus, combining them with our novel calculus results in a new, modular approach for proving non-termination. An empirical evaluation demonstrates the applicability of our approach, both for loop acceleration and for proving non-termination.


翻译:循环加速可以用来证明以整数操作的程序的安全性、可达性、运行时间界限和(非)终止。 为此,已经提出了各种加速技术。 但是,所有这些技术都是单一的:它们要么成功地加速环绕,要么完全失败。相反,我们提出了一个微积分,允许以模块方式将加速技术结合起来,我们展示了如何将许多现有的加速技术纳入我们的微积分。此外,我们提出了两种新的加速技术,可以无缝地融入我们的微积分中。其中一些加速技术只适用于非终止环。因此,将它们与我们的新微积分相结合,形成一种新的模块化方法来证明非终止。一项实证性评价显示了我们的方法,即循环加速和证明非终止的实用性。

0
下载
关闭预览

相关内容

Fariz Darari简明《博弈论Game Theory》介绍,35页ppt
专知会员服务
109+阅读 · 2020年5月15日
专知会员服务
159+阅读 · 2020年1月16日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
MIT新书《强化学习与最优控制》
专知会员服务
275+阅读 · 2019年10月9日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
Reinforcement Learning: An Introduction 2018第二版 500页
CreateAMind
11+阅读 · 2018年4月27日
carla无人驾驶模拟中文项目 carla_simulator_Chinese
CreateAMind
3+阅读 · 2018年1月30日
已删除
将门创投
5+阅读 · 2018年1月24日
论文浅尝 | Leveraging Knowledge Bases in LSTMs
开放知识图谱
6+阅读 · 2017年12月8日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Arxiv
0+阅读 · 2022年1月29日
VIP会员
相关VIP内容
Fariz Darari简明《博弈论Game Theory》介绍,35页ppt
专知会员服务
109+阅读 · 2020年5月15日
专知会员服务
159+阅读 · 2020年1月16日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
MIT新书《强化学习与最优控制》
专知会员服务
275+阅读 · 2019年10月9日
相关资讯
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
Reinforcement Learning: An Introduction 2018第二版 500页
CreateAMind
11+阅读 · 2018年4月27日
carla无人驾驶模拟中文项目 carla_simulator_Chinese
CreateAMind
3+阅读 · 2018年1月30日
已删除
将门创投
5+阅读 · 2018年1月24日
论文浅尝 | Leveraging Knowledge Bases in LSTMs
开放知识图谱
6+阅读 · 2017年12月8日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Top
微信扫码咨询专知VIP会员