Context-aware counter abstraction
Context-aware counter abstraction
复制标题
上下文感知计数器抽象
DOI：
10.1007/s10703-010-0096-7
复制
发表时间：
2010
影响因子：
0.8
通讯作者：
Basler G
中科院分区：
文献类型：
--
作者：
Basler G
多核计算的趋势使得并行软件成为计算机辅助验证的重要目标。不幸的是，这类软件的模型检查器受到组合状态空间爆炸的严重影响。我们展示了如何将计数器抽象应用到真实世界的并发程序中，以消除线程复制造成的冗余。作为局部状态向量的传统全局状态表示被线程计数器向量取代，每个局部状态一个。在实践中，这种想法的直接实现对当地州的数量非常敏感。我们提出了一种新的符号探索算法，通过仔细调度在搜索过程中的任何时刻跟踪哪些计数器来避免这一问题。我们已经在布尔程序上进行了实验，这是由于Slamp项目的成功而促进的抽象。实验证明了我们的方法在实际程序中的适用性，并且与普通的符号状态空间探索和偏序方法优化的探索相比，通常可以获得巨大的节省。据我们所知，我们的工具标志着对具有非平凡局部状态空间的程序的计数器抽象的第一个实现，从而产生了一个用于并发布尔程序的模型检查器，它承诺了真正的可伸缩性。
The trend towards multi-core computing has made concurrent software an important target of computer-aided verification. Unfortunately, Model Checkers for such software suffer tremendously from combinatorial state space explosion. We show how to applycounter abstractionto real-world concurrent programs to factor out redundancy due to thread replication. The traditional global state representation as a vector of local states is replaced by a vector of thread counters, one per local state. In practice, straightforward implementations of this idea are unfavorably sensitive to the number of local states. We present a novel symbolic exploration algorithm that avoids this problem by carefully scheduling which counters to track at any moment during the search. We have carried out experiments on Boolean programs, an abstraction promoted by the success of theSlamproject. The experiments give evidence of the applicability of our method to realistic programs, and of the often huge savings obtained in comparison to plain symbolic state space exploration, and to exploration optimized by partial-order methods. To our knowledge, our tool marks the first implementation of counter abstraction to programs with non-trivial local state spaces, resulting in a Model Checker for concurrent Boolean programs that promises true scalability.
登录
查看更多内容
模型检查中对称性约简的精确和近似策略
DOI：
--
发表时间：
2006
期刊：
World Congress on Formal Methods
影响因子：
--
作者：
Alastair F. Donaldson;Alice Miller
通讯作者：
Alice Miller
动态对称性降低
DOI：
10.1007/978-3-540-31980-1_25
发表时间：
2005
期刊：
ArXiv
影响因子：
--
作者：
E. Allen Emerson;T. Wahl
通讯作者：
T. Wahl
结合对称性约简和欠近似进行符号模型检查
DOI：
--
发表时间：
2002
期刊：
Formal Methods Syst. Des.
影响因子：
--
作者：
S. Barner;O. Grumberg
通讯作者：
O. Grumberg
使用通用代表进行概率模型检查的对称性约简
DOI：
10.1007/11901914_4
发表时间：
2006
期刊：
ACM Comput. Surv.
影响因子：
--
作者：
Alastair F. Donaldson;Alice Miller
通讯作者：
Alice Miller
虚拟对称性降低
DOI：
--
发表时间：
2000
期刊：
Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332)
影响因子：
--
作者：
E. Emerson;John Havlicek;Richard J. Trefler
通讯作者：
Richard J. Trefler