Automatic Abstraction in Symbolic Trajectory Evaluation
Automatic Abstraction in Symbolic Trajectory Evaluation
复制标题
DOI：
10.1109/famcad.2007.27
复制
发表时间：
2007-11
期刊：
影响因子：
--
通讯作者：
Sara Adams;Magnus Björk;T. Melham;C. Seger
中科院分区：
文献类型：
--
作者：
Sara Adams;Magnus Björk;T. Melham;C. Seger
符号轨迹评估（STE）是一种基于抽象状态集格上符号模拟的模型检测技术。STE算法在布尔公式编码的这些抽象的家族上操作，使得在单个模型检查运行中能够验证许多不同的抽象情况。这为实现分区数据抽象提供了一种灵活的方法。它通常被称为“符号索引”，广泛用于内存验证，但在其他地方的采用相对有限，主要是因为用户通常必须手动创建正确的索引抽象族。这项工作提供了第一个已知的算法，自动计算这些分区的抽象给定的参考模型规范。我们的实验结果表明，这种方法不仅简化了存储器验证，而且还可以完全自动地处理完全不同的设计。
Symbolic trajectory evaluation (STE) is a model checking technology based on symbolic simulation over a lattice of abstract state sets. The STE algorithm operates over families of these abstractions encoded by Boolean formulas, enabling verification with many different abstraction cases in a single modelchecking run. This provides a flexible way to achieve partitioned data abstraction. It is usually called "symbolic indexing' and is widely used in memory verification, but has seen relatively limited adoption elsewhere, primarily because users typically have to create the right indexed family of abstractions manually. This work provides the first known algorithm that automatically computes these partitioned abstractions given a reference-model specification. Our experimental results show that this approach not only simplifies memory verification, but also enables handling completely different designs fully automatically.