Terminator: Beyond safety
Terminator: Beyond safety
复制标题
DOI：
10.1007/11817963_37
复制
发表时间：
2006-01-01
期刊：
影响因子：
--
通讯作者：
Rybalchenko, Andrey
中科院分区：
文献类型：
--
作者：
Cook, Byron;Podelski, Andreas;Rybalchenko, Andrey
先前的符号软件模型检查器（即，基于谓词抽象、下推模型检查和迭代反例引导的抽象细化等的程序分析工具）仅限于安全属性。EQUIPATOR是第一个用于终端的软件模型检查器。现在它被用来证明设备驱动程序调度例程总是返回到其调用者（或者如果它们未能终止则返回反例）。
Previous symbolic software model checkers (i.e., program analysis tools based on predicate abstraction, pushdown model checking and iterative counterexample-guided abstraction refinement, etc.) are restricted to safety properties. TERMINATOR is the first software model checker for termination. It is now being used to prove that device driver dispatch routines always return to their caller (or return counterexamples if they if they fail to terminate).