[pl-seminar] Practice talk 7-18-05

[Nick Kidd <kidd@xxxxxxxxxxx>]

Hello,

I will be giving a presentation tomorrow morning at 10 am in room  
2351. This is a practice talk for an upcoming visit to MSR. The talk  
length is ~ 45 minutes. Any feedback will be appreciated. Cookies  
will be served.

Thanks,
-Nick

Title:
Model-Checking Concurrent Message-Passing C Programs with Recursive  
Calls

Abstract:

We extend the model-checker MAGIC so that it can handle concurrent  
recursive programs. We model such programs using "communicating  
pushdown systems", and reduce the reachability problem for this model  
to deciding the emptiness of the intersection of two context free  
languages L1 and L2. We tackle this undecidable problem using a  
Counter Example Guided Abstraction Refinement (CEGAR) scheme based on  
(1) computing over-approximations A1 and A2 of L1 and L2, (2)  
checking if the intersection of A1 and A2 is non-empty, and if the  
non-empty intersection represents an infeasible trace, (3) refining  
these overapproximations A1 and A2. Finally, we impart lessons  
learned from implementing our system.

This is joint work with Sagar Chaki, Edmund Clarke, Thomas Reps, and  
Tayssir Touili.