Type-directed Bounding of Collections in Reactive Programs
Type-directed Bounding of Collections in Reactive Programs
复制标题
DOI：
10.1007/978-3-030-11245-5_13
复制
发表时间：
2018-10
期刊：
影响因子：
--
通讯作者：
Tianhan Lu;Pavol Cerný;B. E. Chang;Ashutosh Trivedi
中科院分区：
文献类型：
--
作者：
Tianhan Lu;Pavol Cerný;B. E. Chang;Ashutosh Trivedi
我们的目标是静态验证，在一个给定的反应式程序中，集合变量的长度不会超过一个给定的界限。我们提出了一个可扩展的基于类型的技术，检查每个集合变量有一个给定的细化类型，指定其长度的约束。我们的细化类型的一个新特性是，细化可以引用吐司计数器，该计数器跟踪AST节点执行了多少次。此功能使类型细化能够跟踪有限的流敏感信息。我们生成验证条件，以确保AST计数器的使用一致，并且类型暗示给定的界限。验证条件由现成的SMT求解器排出。实验结果表明，我们的技术是可扩展的，有效地验证反应式程序的集合长度的要求。
Our aim is to statically verify that in a given reactive program, the length of collection variables does not grow beyond a given bound. We propose a scalable type-based technique that checks that each collection variable has a given refinement type that specifies constraints about its length. A novel feature of our refinement types is that the refinements can refer toAST countersthat track how many times an AST node has been executed. This feature enables type refinements to track limited flow-sensitive information. We generate verification conditions that ensure that the AST counters are used consistently, and that the types imply the given bound. The verification conditions are discharged by an off-the-shelf SMT solver. Experimental results demonstrate that our technique is scalable, and effective at verifying reactive programs with respect to requirements on length of collections.