Sciweavers

CAV
2006
Springer

Terminator: Beyond Safety

14 years 2 months ago
Terminator: Beyond Safety
Previous symbolic software model checkers (i.e., program analysis tools based on predicate abstraction, pushdown model checkiterative 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).
Byron Cook, Andreas Podelski, Andrey Rybalchenko
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where CAV
Authors Byron Cook, Andreas Podelski, Andrey Rybalchenko
Comments (0)