The purpose of the course project is to help you integrate what you have learned in the course, and to engage you in research in the area of computer-aided reasoning for software. We will take a broad view of what “software” and “programs” are. This, of course, includes code in a programming language. But you can also apply computer-aided reasoning to biological systems (where programs may be models of cell processes), to hardware (where programs may be protocols or memory models), and to education (where programs may be geometry constructions). Your project can automate a programming task (such as verification, synthesis, and debugging), or support a new kind of programming construct (such as angelic choice). The possibilities are endless—so, think big!
The project will include 4 milestones. All milestone deliverables should be submitted by one member of each team.
|Writing a proposal||1–2 page paper||23:00 on Apr 27|
|Developing a prototype||Prototype source code||23:00 on Jun 01|
|Demoing the prototype||Slide presentation and demo||11:30 on Jun 01|
|Writing a report||5 page paper||23:00 on Jun 01|
Writing a proposal
The first step is to form a team of 2–3 students. This should be easy, but if you are having trouble, talk to the staff.
Next, choose a topic together with your teammates. Choosing a topic is not as difficult as it may seem. The key is to generate as many ideas as you can, without thinking about whether it is possible to implement them. Just think of tools you would like to use or to build, and the instructor can help you define the problem so that you can complete the project in 7 weeks. If your find yourself stuck in the idea-generating state, schedule a meeting with the instructor (well before Apr 27).
Once you have chosen a topic, write a 1–2 page proposal to flesh out your ideas. The proposal should include a precise statement of the problem you are solving; a brief literature survey; and a timeline for developing the prototype. Use a 10pt font to typeset the proposal, and submit it, in PDF format, by 23:00 on Apr 27.
Developing a prototype
Start developing your prototype as soon as possible. Do not wait until the last week or two of the quarter! Computer-aided tools are not easy to build, and you will almost certainly run into engineering and performance problems. The instructor will help you come up with solutions, but you will need time to implement them.
Concentrate on getting your tool to work on a few end-to-end scenarios. This is what you want to demo. Seven weeks is (generally) not enough time to develop a robust tool that will work for all use cases. Your goal is to convincingly demonstrate the potential of your idea, and to be able to articulate, in the final report, how your prototype could be extended to a usable tool.
What if your idea doesn’t work out, and you realize your tool will never scale to real problems? That’s okay! This is exploratory research, and as long as you can clearly explain your negative result, you will still get credit for the work.
Presenting your tool
You will demo your tool during the final lecture (Jun 01). Aim to show it working on one or two engaging end-to-end scenarios. Prepare a a few slides that describe your project, and be ready to explain your technical contribution in 8 minutes. Every member of the team must present.
Writing the final report
The purpose of the final report is to present your ideas, algorithms, implementation, and experiences—what worked and what didn’t. It should include the following sections:
- Introduction and problem statement.
- Overview of your approach and a summary of how it relates to previous work.
- Algorithms and Logical Encodings you developed.
- Summary of Results, including key design and implementation challenges; how you addressed them (what worked, what didn’t, and why); and how this work could lead to a real tool or a full-length conference paper.
- Teamwork: a one-paragraph description of the individual team member’s contributions.
- Course Topics: a one-paragraph description of the course topics applied in the project, and a one-paragraph description (if applicable) of any topics that would have been useful but weren’t covered in the course.
The report should be 5 pages long (excluding references), typeset with a 10pt font. Keep your writing brief and precise. Illustrate algorithms and encodings with examples and figures. Illustrate results with tables, graphs, and screenshots.
Submit the report, in PDF format, by 23:00 on Jun 01. The final submission should also include your demo slides and a ZIP archive with the source code for the tool, build scripts, benchmarks (if applicable), and a README file describing how to run the tool on your end-to-end scenarios.