Multithreaded-Cartesian Abstract Interpretation of Multithreaded Recursive Programs Is Polynomial

Abstract Undecidability is the scourge of verification for many program classes. We consider the class of shared-memory multithreaded programs in the interleaving semantics such that the number of threads is finite and con-stant throughout all executions, each thread has an unbounded stack, and the shared memory and the stack-frame memory are finite. Verifying that a given program state does not occur in executions of such a program is undecidable. We show that the complexity of verification drops to polynomial time un-der multithreaded-Cartesian abstraction. Furthermore, we demonstrate that multithreaded-Cartesian abstract interpretation generates an inductive in-variant which is a regular language. Under logarithmic cost measure, both proving non-reachability and creating a finite automaton can be attained in O(n log2 n) time in the number of threads n and in polynomial time in all other quantities.