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

Vineet Kahlon, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

19 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings - 21st Annual IEEE Symposium on Logic in Computer Science, LICS 2006
Pages101-110
Number of pages10
DOIs
StatePublished - Dec 1 2006
Externally publishedYes
Event21st Annual IEEE Symposium on Logic in Computer Science, LICS 2006 - Seattle, WA, United States
Duration: Aug 12 2006Aug 15 2006

Publication series

NameProceedings - Symposium on Logic in Computer Science
ISSN (Print)1043-6871

Other

Other21st Annual IEEE Symposium on Logic in Computer Science, LICS 2006
CountryUnited States
CitySeattle, WA
Period8/12/068/15/06

All Science Journal Classification (ASJC) codes

  • Software
  • Mathematics(all)

Fingerprint Dive into the research topics of 'An automata-theoretic approach for model checking threads for LTL properties'. Together they form a unique fingerprint.

Cite this