
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
 Abstractionbased
techniques for verification
 Compositional
verification
 Realtime
model checking
 Hybrid
systems model checking
 Runtime
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 verificationrelated
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 realtime
 Prism. Model checker for probabilistic systems
 Reactis®. Validation tool for realtime 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 presentationtopic projects,
are the essential contributions of the papers understood and clearly
articulated? For casestudy 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 eyecontact
maintained? Is the material
wellorganized? 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?