Research projects should be in one of the following forms:
- Specify and implement a system using verification tools
such as Z3, Rosette, Dafny, and Coq, and formally verify
that the implementation meets the specification.
- Build a tool that systematically uncovers correctness
issues of existing software or system configurations.
- Conduct an empirical study of formally verified systems and
analyze their assumptions and specifications in end-to-end systems.
The project may be done individually or in a group of two to three.
You’ll turn in your code and a paper describing the design and
which we will post on the course website (unless you explicitly
talk to us about why you want to keep it confidential).
Use the OSDI’16 submission format
for your paper.
April 15: submit your project proposal, up to one page.
May 13: checkpoint:
please upload a PDF describing your progress on achieving the goals
you included in your proposal. Clearly explain any changes you
have made to the goal of your project based on your experience so
far. Include examples that your prototype can already handle.
Provide a clear, concrete plan of what you will need to accomplish
in the remaining weeks to complete your project and what we can
expect to see in the presentation.
June 9/10: demo.
June 10: project report due.
Here is a list of ideas to get you started thinking. Feel free to
pursue your own ideas.
- Specify and do something useful with hardware primitives, such
as Intel’s SGX, transactional memory, and virtualization.
- Build a verified storage system, such as a key-value store, a
SQL database, and a file system.
- Bootstrap a verified compiler through self hosting.
- Implement and verify a cryptographic protocol, such as TLS and tcpcrypt.
- Implement and verify a distributed hash table.
- Implement and verify Bitcoin’s scripting system for transactions.
- Replicate FSCQ in Dafny. Report on what was easier and what was harder.
- Take a large collection of lemmas from a verified system, such as Ironclad or Verdi.
Prove them using another tool.
- Build a message fragmentation layer for Ironclad/Verdi. Prove it correct. Bonus: Prove it live.
- Specify and verify the safety and liveness of some variant of Paxos.
Relatively easy examples include:
Disk Paxos, or
Harder examples include
- Build and verify a high-performance B (or B+) tree implementation. Compare with unverified versions.
- Check out the challenge problems in assignments.
- Check out the ideas and projects from
Penn’s CIS 670 and