Current Projects
- CCAC: Verification of Transactional Memory
- LSS: Language-based Software Security
- Fully-verified Thread Library
- Certifying Compilers for C-like Languages
Past Projects
- RCAL86: Realistic Certifying Assembly Language for IA32. (Finished in Sep 2006)
- TLL: Typed Low-level Language for Open Runtime Platform. (Finished in Sep 2004)
Other Projects
We have also done other projects on Advanced Type System, Program Analysis, etc.