Provably correct software is one of the key challenges in our softwaredriven society. While formal verification establishes the correctness of a given program, the result of program synthesis is a program which is correct by construction. In this paper we overview some of our results for both of these scenarios when analysing programs with loops. The class of loops we consider can be modelled by a system of linear recurrence equations with constant coefficients, called C-finite recurrences. We first describe an algorithmic approach for synthesising all polynomial equality invariants of such non-deterministic numeric single-path loops. By reverse engineering invariant synthesis, we then describe an automated method for synthesising program loops satisfying a given set of polynomial loop invariants. Our results have applications towards proving partial correctness of programs, compiler optimisation and generating number sequences from algebraic relations. This is a preprint that was invited for publication at VMCAI 2021.


翻译:正确无误的软件是软件驱动社会的主要挑战之一。 虽然正式的核查可以确定特定程序的正确性, 程序合成的结果是一个构建正确的程序。 在本文中, 在用环状分析程序时, 我们浏览了两种方案的结果。 我们所考虑的循环类别可以通过一个具有常数的线性重复复现方程式系统( 称为C- 无限复现)来模拟。 我们首先描述一种算法方法, 用于合成非确定性数字单路径环中所有多数值平等的变量。 通过逆向工程合成, 我们然后描述一个合成程序循环的自动方法, 满足了一组给定的多数值圈变量。 我们的结果可以用来证明程序的部分正确性, 编译器优化, 并生成代数关系中的序列。 这是在 VMCAI 2021 上邀请出版的预印本 。

0
下载
关闭预览

相关内容

VMCAI为来自验证、模型检验和抽象解释社区的研究人员提供了一个论坛,促进了交互作用、相互启发和结合这些领域和相关领域的混合方法的发展。VMCAI2019将是该系列的第20版。 官网链接:https://popl19.sigplan.org/track/VMCAI-2019
Linux导论,Introduction to Linux,96页ppt
专知会员服务
75+阅读 · 2020年7月26日
Fariz Darari简明《博弈论Game Theory》介绍,35页ppt
专知会员服务
104+阅读 · 2020年5月15日
Python计算导论,560页pdf,Introduction to Computing Using Python
专知会员服务
69+阅读 · 2020年5月5日
【新书】Java企业微服务,Enterprise Java Microservices,272页pdf
【新书】Python编程基础,669页pdf
专知会员服务
186+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
Hierarchically Structured Meta-learning
CreateAMind
23+阅读 · 2019年5月22日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
41+阅读 · 2019年1月3日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
15+阅读 · 2018年12月24日
carla 学习笔记
CreateAMind
9+阅读 · 2018年2月7日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
最佳实践:深度学习用于自然语言处理(三)
待字闺中
3+阅读 · 2017年8月20日
Arxiv
0+阅读 · 2021年4月29日
Arxiv
0+阅读 · 2021年4月28日
Efficient and Effective $L_0$ Feature Selection
Arxiv
5+阅读 · 2018年8月7日
VIP会员
相关资讯
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
Hierarchically Structured Meta-learning
CreateAMind
23+阅读 · 2019年5月22日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
41+阅读 · 2019年1月3日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
15+阅读 · 2018年12月24日
carla 学习笔记
CreateAMind
9+阅读 · 2018年2月7日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
最佳实践:深度学习用于自然语言处理(三)
待字闺中
3+阅读 · 2017年8月20日
Top
微信扫码咨询专知VIP会员