Only graduate students in CISC422/853 need to work on a project.
Groups
The projects for CISC853 can be worked on in groups of 1 or 2 students.
Reports
Please use the ACM SIG Proceedings format when preparing your
project summaries. Templates for Word, Word Perfect, Latex
are available
here
Project suggestions
Other model checkers (Java PathFinder, SMV, ...)
More on the theory behind model checking: E.g.,
how to translate LTL into Buechi Automata,
complexity, optimizations (e.g., different abstraction techniques)
Heuristics in model checking
Advanced Spin:
Embedding C code into Promela models
Dealing with fairness assumptions
Applications of model checking to other domains (e.g.,
security, web applications, business processes, real-time systems,
probabilistic systems)
Other formal analysis techniques or tools:
DART: Directed Automated Random Testing.
P. Godefoid, Nils Klarlund and Koushik Sen.
Proceedings of ACM SIGPLAN 2005 Conference on
Programming Language Design and Implementation (PLDI 2005),
pages 213-223, Chicago, June 2005.
Available
here.
Bhargav Gulavani, Thomas A. Henzinger, Yamini Kannan, Aditya Nori, and Sriram K. Rajamani.
Synergy: A new algorithm for property checking. Proceedings of the 14th Annual
Symposium on Foundations of Software Engineering (FSE), ACM Press, 2006.
Available
here.
Perracotta: Mining Temporal API Rules from Imperfect Traces.
Also, I'm open to other project suggestions; make sure you discuss the
details with me first.
Deliverables
For each project given out, I expect a 2 page project proposal, a
20 minute presentation and a summary paper with at least 2, but not
more than 5 pages.
Presentations will take place in the week right after the end of classes.
Summary papers will be due on the day of the presentation.