CMSC 838M Spring 2017 Model Checking Project Ideas

 

 

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

·       Model checking of embedded systems / cyber-physical systems

·       Verification and systems biology

·       Numerical verification

·       Statistical model checking

·       Bounded model checking

·       Case studies

·       Model checking for real design languages, e.g. Simulink, SysML, SystemC, …

·       Synthesis from specifications

·       Mu-calculus model checking

 

This is just a list 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®.  V&V 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.

·       C2E2.  Hybrid systems verification tool

·       KeYmaera.  Interactive verification tool for hybrid systems.

·       mCRL2.  Refinement-checking tool for distributed systems.

·       Java Pathfinder.  Run-time verification tool for Java.

·       Dafny.  A tool for verifying programs.

·       CBMC.  A bounded model-checking tool for C.

 

More tools are listed here.  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?