期刊文献+
共找到1篇文章
< 1 >
每页显示 20 50 100
Lazy Slicing for State-Space Exploration 被引量:1
1
作者 黄少滨 黄宏涛 +2 位作者 陈志远 吕天阳 张涛 《Journal of Computer Science & Technology》 SCIE EI CSCD 2012年第4期872-890,共19页
CEGAR (Counterexample-guided abstraction refinement)-based slicing is one of the most important techniques in reducing the state space in model checking. However, CEGAR-based slicing repeatedly explores the state sp... CEGAR (Counterexample-guided abstraction refinement)-based slicing is one of the most important techniques in reducing the state space in model checking. However, CEGAR-based slicing repeatedly explores the state space handled previously in case a spurious counterexample is found. Inspired by lazy abstraction, we introduce the concept of lazy slicing which eliminates this repeated computation. Lazy slicing is done on-the-fly, and only up to the precision necessary to rule out spurious counterexamples. It identifies a spurious counterexample by concretizing a path fragment other than the full path, which reduces the cost of spurious counterexample decision significantly. Besides, we present an improved over-approximate slicing method to build a more precise slice model. We also provide the proof of the correctness and the termination of lazy slicing, and implement a prototype model checker to verify safety property. Experimental results show that lazy slicing scales to larger systems than CEGAR-based slicing methods. 展开更多
关键词 counterexample-guided abstraction refinement spurious counterexample over-approximate slicing local refinement lazy slicing
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部