Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Twenty-First Annual IEEE Symposium on

Logic in Computer Science (LICS 2006)

Paper: An Automata-theoretic Appraoch for Model Checking Threads for LTL Properties (at LICS 2006)

Authors: Vineet Kahlon Aarti Gupta

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 [1]. 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.

BibTeX

  @InProceedings{KahlonGupta-AnAutomatatheoretic,
    author = 	 {Vineet Kahlon and Aarti Gupta},
    title = 	 {An Automata-theoretic  Appraoch for Model Checking Threads for LTL Properties},
    booktitle =  {Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science (LICS 2006)},
    year =	 {2006},
    month =	 {August}, 
    pages =      {101--110},
    location =   {Seattle, Washington, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2017-04-0512:37
Andrzej Murawski