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

[Nick Kidd <kidd@xxxxxxxxxxx>]

I apologize for the typo, the talk is in room 2310.

Thanks,
-Nick

On Jul 17, 2005, at 4:25 PM, Nick Kidd wrote:

> 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.
>
> _______________________________________________
> Pl-seminar mailing list
> Pl-seminar@xxxxxxxxxxx
> https://lists.cs.wisc.edu/mailman/listinfo/pl-seminar