[pl-seminar] Practice talk today @ 4:30 in 4310

[Nick Kidd <kidd@xxxxxxxxxxx>]

Hello,

I invite you to attend a practice talk today at 4:30 in room 4310.
The talk is 25 minutes long with 5 minutes at the end for questions.
I am looking for comments on the material, presentation, etc. Any  
comments
and criticism are appreciated. This is a shortened version of a 50 min.
practice talk I gave a few weeks ago.

Thanks,
-Nick


Title: Verifying Concurrent Message-Passing C Programs with Recursive  
Calls
Abstract
------------------------------------------------------------------------ 
------------------------------
We consider the model-checking problem for C programs with (1) data
ranging over very large domains, (2) (recursive) procedure calls, and
(3) concurrent parallel components that communicate via synchronizing
actions. 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
CounterExample Guided Abstraction Refinement (CEGAR) scheme. We
implemented our technique in the model checker MAGIC and found a
previously unknown bug in a version of a Windows NT Bluetooth driver.

Attachment: smime.p7s
Description: S/MIME cryptographic signature