Complexity of pattern-based verification for multithreaded programs

Javier Esparza, Pierre Ganty

Research output: Contribution to journalArticlepeer-review

20 Scopus citations


Pattern-based verification checks the correctness of the program executions that follow a given pattern, a regular expression over the alphabet of program transitions of the form w*1 : : :w*n. For multithreaded programs, the alphabet of the pattern is given by the synchronization operations between threads. We study the complexity of pattern-based verification for abstracted multithreaded programs in which, as usual in program analysis, conditions have been replaced by nondeterminism (the technique works also for boolean programs). While unrestricted verification is undecidable for abstracted multithreaded programs with recursive procedures and PSPACE-complete for abstracted multithreaded while-programs, we show that pattern-based verification is NP-complete for both classes. We then conduct a multiparameter analysis in which we study the complexity in the number of threads, the number of procedures per thread, the size of the procedures, and the size of the pattern. We first show that no algorithm for pattern-based verification can be polynomial in the number of threads, procedures per thread, or the size of the pattern (unless P=NP). Then, using recent results about Parikh images of regular languages and semilinear sets, we present an algorithm exponential in the number of threads, procedures per thread, and size of the pattern, but polynomial in the size of the procedures.

Original languageEnglish
Pages (from-to)499-510
Number of pages12
JournalACM SIGPLAN Notices
Issue number1
StatePublished - Jan 2011


  • Concurrent programming
  • Context-free languages
  • Safety


Dive into the research topics of 'Complexity of pattern-based verification for multithreaded programs'. Together they form a unique fingerprint.

Cite this