Efficient Symbolic Representations for Arithmetic Constraints in Verification
Efficient Symbolic Representations for Arithmetic Constraints in Verification
复制标题
验证中算术约束的有效符号表示
DOI：
--
复制
发表时间：
2003
影响因子：
0.8
通讯作者：
T. Bultan
中科院分区：
文献类型：
--
作者：
Constantinos Bartzis;T. Bultan
在本文中，我们讨论了有效的符号表示的无限状态系统指定使用线性算术约束。我们给出了构造有限自动机的算法，它表示满足线性约束的整数集。这些自动机可以表示有符号或无符号整数，并且与其他类似方法相比具有更少的状态数。我们提出了有效的存储技术的自动机的过渡函数和扩展的布尔和整数变量的公式的构造算法。我们还推导出条件，保证符号验证算法中使用的前置条件计算不会导致自动机大小的指数增加。我们实验比较不同的符号表示，使用它们来验证非平凡的并发系统。实验结果表明，基于我们的构造算法的符号表示优于欧米茄库中使用的多面体表示，和LASH中使用的自动机表示。
In this paper we discuss efficient symbolic representations for infinite-state systems specified using linear arithmetic constraints. We give algorithms for constructing finite automata which represent integer sets that satisfy linear constraints. These automata can represent either signed or unsigned integers and have a lower number of states compared to other similar approaches. We present efficient storage techniques for the transition function of the automata and extend the construction algorithms to formulas on both boolean and integer variables. We also derive conditions which guarantee that the pre-condition computations used in symbolic verification algorithms do not cause an exponential increase in the automata size. We experimentally compare different symbolic representations by using them to verify non-trivial concurrent systems. Experimental results show that the symbolic representations based on our construction algorithms outperform the polyhedral representation used in Omega Library, and the automata representation used in LASH.