Outline of This Talk Background:the Rely-Guarantee Method Challenges for Dynamic Thread Creation/Termination ■Our Approach The CMAP Framework Conclusion and Future Work 2005-9-16 NJPLS@Stevens2005-9-16 NJPLS@Stevens Outline of This Talk ◼ Background: the Rely-Guarantee Method ◼ Challenges for Dynamic Thread Creation/Termination ◼ Our Approach ◼ The CMAP Framework ◼ Conclusion and Future Work