CISC422/853: Formal Methods in Software Engineering: Computer-aided Verification (Winter 2009)

Projects

[Home] [Content] [Schedule] [Readings] [Assignments] [Tools] [Projects] [Messages]

Note

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.
  - Project page
- FindBugs
- Blast: Software model checker for C. Uses automatic abstraction refinemaent.
  - Project page
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.