CS 528/428 Project Ideas and Resources, Spring 2009

This list is incomplete. More project ideas will be added in the next few weeks.

1. Writing a survey paper on a particular topic covered during the lectures.
2. Mechanizing some fancy examples in Reynolds' lecture notes on separation logic in the Coq proof assistant.
3. Apply CSL/RGSep/LRG to certify some common concurrent primitives and idioms (see Herlihy and Shavit book on "the art of multiprocessor programming").
4. Rewrite the proof for the non-blocking stack example (in Parkinson et al POPL'07) using RGSep or LRG.
5. Adding support for thread creation and termination in CSL, RGSep or LRG.
6. Extend LRG so that it can be used to certify the link list example in Chapter 3 and the non-blocking stack example in Chapter 5 of Vafeiadis's PhD dissertation.
7. Revise LRG so that you can eliminate the invariant fence; or extend RGSep so that it can support local reasoning described in the LGR paper.
8. Apply what you learned from CSL, RGSep, and LRG to certify some examples used in the Sing# paper in EuroSys'07 (or the Luna paper).
9. Extend CSL to support a notion of principal as you often seen in the papers on information flow analysis.
10. Integrate DIFC into the setting of simple imperative language like Imp (as used in the CSL/RGSep/LRG literatures).
11. Formalize some fragments of the Asbestos labels or the HiStar labels, and explain how they are related to the standard DIFC labels.
12. Read the CCAP paper by Yu and Shao, and the TAL for Confidentiality paper by Yu and Islam, and show how you might use rely-guarantee reasoning in one to prove the "non-interference" property in another.
13. Adapt the work on relaxed noninterference by Li and Zdancewic in POPL'05 to the setting of a simple imperative language (with separation logic or CSL) or a low-level assembly language.
14. Research how declassification is related to rely-guarantee reasoning.
15. Certify a simple device driver in the AIM framework (Feng et al PLDI'08); or certify the implementation of a few more synchronization primitives (e.g., message passing) in AIM.
16. Some embeded OS, like TinyOS or SOS, use event driven model instead of the thread model to support concurrency. Can you design a machine which supports the event-driven model? How different it will be with CCAP/CMAP? Here is a paper which uses Rely/Guarantee method to verify event-driven programs.
18. ......