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).

• Type: Conference
• Year: 2006
• Where: CAV
• Authors: Byron Cook, Andreas Podelski, Andrey Rybalchenko
• Keywords: CAV 2006, Counterexample-guided Abstraction Refinement, Hardware, Software Model Checker, Symbolic Software Model