|
Published Articles >> Table of Contents >> Abstract
21st Annual IEEE Symposium on Logic in Computer Science (LICS'06)
pp. 101-110
An Automata-Theoretic Approach for Model Checking Threads for LTL Propert
Vineet Kahlon, NEC Labs America, USA
Aarti Gupta, NEC Labs America, USA
Full Article Text:
 
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2006.11
Send link to a friend
| 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.
|
 Additional Information
|
Citation:
Vineet Kahlon, Aarti Gupta,
"An Automata-Theoretic Approach for Model Checking Threads for LTL Propert,"
lics,
pp. 101-110,
21st Annual IEEE Symposium on Logic in Computer Science (LICS'06),
2006
|
|
