In program verification, constraint-based random testing is a powerful technique which aims at generating random test cases that satisfy functional properties of a program. However, on recursive constrained data-structures (e.g., sorted lists, binary search trees, quadtrees), and, more generally, when the structures are highly constrained, generating uniformly distributed inputs is difficult. In this paper, we present Testify: a framework in which users can define algebraic data-types decorated with high-level constraints. These constraints are interpreted as membership predicates that restrict the set of inhabitants of the type. From these definitions, Testify automatically synthesises a partial specification of the program so that no function produces a value that violates the constraints (e.g. a binary search tree where nodes are improperly inserted). Our framework augments the original program with tests that check such properties. To achieve that, we automatically produce uniform random samplers that generate values which satisfy the constraints, and verifies the validity of the outputs of the tested functions. By generating the shape of a recursive data-structure using Boltzmann sampling and generating evenly distributed finite domain variable values using constraint solving, our framework guarantees size-constrained uniform sampling of test cases. We provide use-cases of our framework on several key data structures that are of practical relevance for developers. Experiments show encouraging results.


翻译:在程序核查中,基于约束的随机测试是一种强大的技术,旨在生成随机测试案例,满足程序功能特性。然而,对于循环约束的数据结构(例如分类列表、二进制搜索树、四叶树),以及更一般地说,当结构高度限制时,很难产生统一分布的输入。在本文件中,我们提出验证:用户可以用来定义代数数据类型的框架,在高层次限制下标注数据类型。这些限制被解释为会籍前提,限制该类居民的组合。根据这些定义,测试自动合成程序的部分规格,以便没有任何功能产生违反限制值(例如,分类列表、二进制搜索树、四叶树),更一般地说,当结构高度限制时,则生成统一分布的分布式数据类型。为了实现这一点,我们自动生成统一的随机抽样样本,从而满足限制,并验证测试函数的正确性。通过这些定义,通过Boltzmann取样和生成均衡分布式的数据结构,从而产生一个违反限制度的值(例如,在节点中插入节点插入一个二进式关键域内值的测试框架),我们使用一些统一的实验性标准。

0
下载
关闭预览

相关内容

不可错过!《机器学习100讲》课程,UBC Mark Schmidt讲授
专知会员服务
72+阅读 · 2022年6月28日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
VCIP 2022 Call for Special Session Proposals
CCF多媒体专委会
1+阅读 · 2022年4月1日
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日
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+阅读 · 2015年12月31日
国家自然科学基金
3+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
1+阅读 · 2009年12月31日
Arxiv
0+阅读 · 2022年10月14日
VIP会员
相关资讯
VCIP 2022 Call for Demos
CCF多媒体专委会
1+阅读 · 2022年6月6日
VCIP 2022 Call for Special Session Proposals
CCF多媒体专委会
1+阅读 · 2022年4月1日
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日
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+阅读 · 2015年12月31日
国家自然科学基金
3+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
1+阅读 · 2009年12月31日
Top
微信扫码咨询专知VIP会员