cs6964: Project Suggestions

Prove theorems in formal language theory (e.g., the pumping lemma for regular languages, closure properties, Myhill-Nerode theorem, ...)
Formalize a mathematical theory, e.g., groups, lattices, number theory, etc.
Formalize key operating system concepts
Automate termination proofs of recursive algorithms.
Verify functional programs. Examples: sorting algorithms, search algorithms, Red-Black trees, compression algorithms, the SML Substring library, the unification algorithm.
Verify hardware algorithms. Examples: fast adders, fast multiplers, etc.
Prove the correctness of a compiler for a simple programming language.
Automate standard operational semantics proofs (e.g. type preservation under execution).
A project of your own choice (I'll have to be convinced it's do-able).