CMSC 630 --- Foundations of Software Verification Spring 2015 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.

Ideas for Presentation Topics

• SAT solvers
• Satisfaction Modulo Theories (SMT) solvers
• Probabilistic model checking
• Verification using theorem provers
• Model checking of source code / hardware designs / communications protocols
• Abstraction-based techniques for verification
• Compositional verification
• Real-time model checking
• Hybrid systems model checking
• Run-time verification
• Model checking and systems biology
• Verification and embedded systems
• Symbolic execution
• Verification and systems biology
• Numerical verification
• Statistical model checking
• Bounded model checking

 

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
• SATABS.  Model checker for C
• SLAM.  Verifier for C programs from Microsoft
• Uppaal.  Model checker for real-time
• Prism.  Model checker for probabilistic systems
• Reactis®.  Validation tool for real-time control systems in MATLAB® / Simulink® / Stateflow®
• Design Verifier.  Another MATLAB / Simulink / Stateflow verification and validation tool.
• SCADE.  Modeling environment for synchronous systems
• PVS.  Interactive specification and verification tool.
• HOL.  General theorem prover also used for verification.
• SpaceEx.  Analysis platform for hybrid systems.
• KeYmaera.  Interactive verification tool for hybrid 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 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?