CMSC 630 --- Theory of Programming Languages Spring 2007 Projects

This page lists some ideas for course projects. Generally, a project may take one of two forms:

• Paper presentation. A topic is selected, 2—3 papers on the topic read, and a presentation given in class
• Case study. A verification tool and system for modeling is selected, the system verified, and a presentation given in class about the results.

Presentation Topics

• Probabilistic model checking
• Verification using theorem provers
• Hoare logics for message-passing systems
• Model checking of source code
• Model checking of hardware designs
• Abstraction-based techniques for verification
• Compositional verification

This is just a smattering of possible verification-related topics; there are many others. Feel free to propose another topic not on this list.

Tools

• NuSMV. Model checker for CTL
• Spin. Model checker for LTL
• Uppaal. Model checker for real-time
• Prism. Model checker for probabilistic systems
• Reactis®. Validation tool for real-time control systems
• SCADE. Modeling environment for synchronous systems

There are other tools as well. Feel free to investigate and propose an alternative.

Project Grading

Your project grade will be based on the following factors, weighted as indicated.

• Depth of understanding: 70%

Is mastery of the material shown? For presentation-topic projects, are the essential contributions of the papers understood and clearly articulated? For case-study projects, are relevant aspects of the system verified, and are features and limitations of the tool well described? Are questions well handled? Is the work presented placed in context of other work?

• Presentation skills: 30%

Does the speaker interact well with the audience? Is appropriate eye-contact maintained? Is the material well-organized? Are the slides clear and well structured? Is appropriate use of graphics and figures (either in slides or on the board) made during the presentation?