CMSC 630 --- Foundations of Software Verification
This page lists some ideas for course projects. Generally, a project may take one of two
presentation. A topic is
selected, 2 – 3 papers on the topic read, and a presentation given in
study. A verification tool and
system for modeling is selected, the system verified, and a presentation
given in class about the results.
Modulo Theories (SMT) solvers
using theorem provers
checking of source code / hardware designs / communications protocols
techniques for verification
systems model checking
checking and systems biology
and embedded systems
and systems biology
This is just a smattering of possible verification-related
topics; there are many others. Feel free
to propose another topic not on this list.
- 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®
Verifier. Another MATLAB /
Simulink / Stateflow verification and validation tool.
- SCADE. Modeling environment for synchronous
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
There are other tools as well. Feel free to investigate and propose an
Your project grade will be based on the following factors,
weighted as indicated.
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?
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?