An automata-theoretic approach for model checking threads for LTL properties

In this paper, we propose a new technique for the verification of concurrent multi-threaded programs. In general, the problem is known to be undecidable even for programs with just two threads [I]. However, we exploit the observation that, in practice, a large fraction of concurrent programs can either be modeled as Pushdown Systems communicating solely using locks or can be reduced to such systems by applying standard abstract interpretation techniques or by exploiting separation of data from control. Moreover, standard programming practice guidelines typically recommend that programs use locks in a nested fashion, In fact, in languages like Java and C#, locks are guaranteed to be nested. For such a framework, we show, by using the new concept of Lock Constrained Multi-Automata Pair (LMAP), that pre*-closures of regular sets of states can be computed efficiently. This is accomplished by reducing the pre*-closure computation for a regular set of states of a concurrent program with nested locks to those for its individual threads. Leveraging this new technique then allows us to formulate a fully automatic, efficient and exact (sound and complete) decision procedure for model checking threads communicating via nested locks for indexed linear-time temporal logic formulae.