Provably correct software is one of the key challenges of our software-driven society. Program synthesis -- the task of constructing a program satisfying a given specification -- is one strategy for achieving this. The result of this task is then a program which is correct by design. As in the domain of program verification, handling loops is one of the main ingredients to a successful synthesis procedure. We present an algorithm for synthesizing loops satisfying a given polynomial loop invariant. The class of loops we are considering can be modeled by a system of algebraic recurrence equations with constant coefficients, encoding thus program loops with affine operations among program variables. We turn the task of loop synthesis into a polynomial constraint problem, by precisely characterizing the set of all loops satisfying the given invariant. We prove soundness of our approach, as well as its completeness with respect to an a priori fixed upper bound on the number of program variables. Our work has applications towards synthesizing loops satisfying a given polynomial loop invariant, program verification, as well as generating number sequences from algebraic relations. To understand viability of the methodology and heuristics for synthesizing loops, we implement and evaluate the method using the Absynth tool.


翻译:正确无误的软件是我们软件驱动社会的关键挑战之一。 程序合成 -- -- 构建一个符合特定规格的程序的任务 -- -- 是实现这一目标的一种战略。 任务的结果是一个设计正确的程序。 正如在程序核查领域一样, 处理环是成功合成程序的主要成份之一。 我们展示了一个合成循环的合成算法, 满足给定的多元循环的变异性。 我们考虑的循环类别可以通过一个具有恒定系数的代数复现方程系统进行模拟, 从而将程序循环与程序变量之间的折叠操作进行编码。 我们把环合成的任务转换成一个多重制约问题, 精确地描述满足给定变量的所有环的特性。 我们证明了我们的方法的正确性, 以及它对于程序变量数的先前固定上限的完整性。 我们的工作应用于合成循环系统, 满足给定的多数值循环, 程序核查, 从而在程序变量之间编码程序循环中进行折合操作。 我们把环合成的任务变成一个多数值制约问题, 通过精确地描述满足给定的环形环形的特性, 来评估我们如何运用它的方法, 。

0
下载
关闭预览

相关内容

专知会员服务
50+阅读 · 2020年12月14日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
IEEE ICKG 2022: Call for Papers
机器学习与推荐算法
3+阅读 · 2022年3月30日
ACM MM 2022 Call for Papers
CCF多媒体专委会
5+阅读 · 2022年3月29日
IEEE TII Call For Papers
CCF多媒体专委会
3+阅读 · 2022年3月24日
ACM TOMM Call for Papers
CCF多媒体专委会
2+阅读 · 2022年3月23日
AIART 2022 Call for Papers
CCF多媒体专委会
1+阅读 · 2022年2月13日
Call for Nominations: 2022 Multimedia Prize Paper Award
CCF多媒体专委会
0+阅读 · 2022年2月12日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Arxiv
0+阅读 · 2022年8月10日
Arxiv
35+阅读 · 2021年8月2日
A Survey of Deep Learning for Scientific Discovery
Arxiv
29+阅读 · 2020年3月26日
VIP会员
相关VIP内容
专知会员服务
50+阅读 · 2020年12月14日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
相关资讯
IEEE ICKG 2022: Call for Papers
机器学习与推荐算法
3+阅读 · 2022年3月30日
ACM MM 2022 Call for Papers
CCF多媒体专委会
5+阅读 · 2022年3月29日
IEEE TII Call For Papers
CCF多媒体专委会
3+阅读 · 2022年3月24日
ACM TOMM Call for Papers
CCF多媒体专委会
2+阅读 · 2022年3月23日
AIART 2022 Call for Papers
CCF多媒体专委会
1+阅读 · 2022年2月13日
Call for Nominations: 2022 Multimedia Prize Paper Award
CCF多媒体专委会
0+阅读 · 2022年2月12日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
相关基金
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员