| Next meeting time and place: 4:30pm, Friday, April 25, N127 | Latest Announcement: ... |
Here is a link to the paper upon which the talk will be based. If I remember correctly, the paper will appear at the PEPM meeting in June in San Diego.
Abstract:
This paper proposes several partial order reduction strategies for
model-checking concurrent object-oriented software that are based on
detecting heap objects that are \emph{thread-local}, i.e., reachable
from a single thread only. We show how thread-local information
appropriate for driving these reductions can be obtained by static
analysis (using adaptations of existing escape analyses). However, we
show that in many cases, existing static analyses targetted to
compiler optimizations fail to detect thread-local information that
can lead to significant savings in model-checking. In fact, we show
that a novel dynamic analysis carried out during model-checking is
actually simpler to implement, and is more effective at reducing
verification costs. These reduction strategies showing upwards of 20
times reduction on realistic programs, and can be easily incorporated
into existing explicit-state software model-checkers.
This is joint work with John Hatcliff, Robby and Venkatesh Prasad Ranganath.