Unbounded-Thread Program Verification using Thread-State Equations

Infinite-state reachability problems arising from unbounded-thread program verification are of great practical importance, yet algorithmically hard. Despite the remarkable success of explicit-state exploration methods to solve such problems, there is a sense that SMT technology can be beneficial to speed up the decision making. This vision was pioneered in recent work by Esparza et al. on SMT-based coverability analysis of Petri nets. We present here an approximate coverability method that operates on thread-transition systems, a model naturally derived from predicate abstractions of multi-threaded programs. In addition to successfully proving uncoverability for all our safe benchmark programs, our approach extends previous work by the ability to decide the wnsafety of many unsafe programs, and to provide a witness path. We also demonstrate experimentally that our method beats all leading explicit-state techniques on safe benchmarks and is competitive on unsafe ones, promising to be a very accurate and fast coverability analyzer.