Comp 681

Formal Methods

Spring 2019

Home Course Info Course Project Readings Tools

Course Project

Milestone Deliverable Due Date
Project Proposal 1 - 2 page paper 2-12-19
Progress Report 3 - 4 page paper 3-21-19
Presentation 15 minutes for content, 5 minutes q&a 5-2-19
Final Report 6 - 10 page final report, code, evaluation material, and any other relevant work 5-6-19

Overview

The course project is the most important component of this class. It can be a theoretical and/or experimental investigation related to topics covered in class. You are also encouraged to pick topics of your own, after consulting with the instructor. It is expected that students team up in groups of 2 or 3 for their project. Projects will culminate in a final paper and presentation.
     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 formal methods, focusing on their applications for software. You should consider building on your strengths and finding ways to leverage other work that you are doing. For instance, if you do work in AI, you might consider how machine learning could be applied to problems of program comprehension or to filtering output from program analysis tools. You also might consider using a project that you are working on, or that you worked on in the past, as a test case for a tool. Synergies with your other work are welcomed!

A non-exhaustive list of types of acceptable projects are:

  • proposing and evaluating a fundamental new technique
  • developing and assessing new algorithms to replace currently-used ones
  • translating a methodology to a new problem domain
  • applying known techniques to new problem domains, such as operating systems, networks, embedded systems, security, biology, aerospace, etc.
  • evaluation of existing techniques or tools, via case studies or controlled experiments
  • port an existing tool to a new domain (e.g., a new programming language or a new version of one)

Writing a Proposal

The first step is to form a team of 2-3 students. Next, choose a topic together with your teammates. Choosing a topic seems daunting, but does not need to be difficult. First, 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 a semester. If your find yourself stuck in the idea-generating state, schedule a meeting with the instructor (well before May 6th).
     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 the project. Use the ACM conference format template, and submit it, in PDF format, by 11:59pm on 2-12.

Progress Report

This is a mid-semester check in that should be 3-4 pages following the ACM conference format. The goal of the progress report is to make sure you have started and address any early challenges.

It should include the following sections:

  • Introduction: Give your brief problem statement and motivation for the work.
  • Technique Design: Give a high level overview of what your techniques is by using an illustrative example. If you have made any algorithms or logical encodings feel free to include them here.
  • Technology: Outline any tools you are using, tools you may use, or tools you are taking inspiration from.
  • Evaluation Plan: Explain what experimental design you plan to do to evaluate your project: is it a quantitative evaluation, qualitative evaluation, both? List questions you plan to ask, and how you will design experiments to answer them.
  • Updated timeline: Give an update on the project progress and adjust your project timeline as needed.

Presenting your Project

Time your presentation for 15 minutes (+5 min for questions). It's very important to finish on time. Practise your presentation several times.

Topics to cover:

  • Motivation, Problem definition, and your approach
  • Related work and what is new about your work
  • Your solution. Describe the main technical challenges and how you tackled them.
  • Hardware/software platform and tools used
  • Demo (optional) -- could be interleaved with the presentation or performed right after
  • Finish with a 1-slide summary: what did you achieve, what more can be done?

Final Report and Project Wrap Up

Your final project report should be written in the style of a conference paper. (You are not required to submit your work to a conference or workshop, but you might choose to do so, and this is the standard of work expected.) Your report should be: 6-10 pages long and follow the ACM conference format template. 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: Give your problem statement and motivation for the work.
  • Related work: Overview of your approach and a summary of how it relates to previous work.
  • Technique: Include content such as algorithms and logical encodings you developed. This can be divided up into multiple sections such as: illustrative example and approach.
  • Evaluation: verview of your experimental design and main results. Also include key design and implementation challenges; how you addressed them (what worked, what didn't, and why).
  • Future Work: What are the next steps that can be taken to continue your work?
  • 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.

llustrate algorithms and models with diagrams, and results with graphs, screenshots, pictures of your hardware, etc. Keep the report short and precise; avoid lengthy and verbose descriptions!
     Submit the report, in PDF format, by 11:59 pm on May 6th. 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.

Note on implementations: If making a tool, concentrate on getting your tool to work on a few end-to-end scenarios, not focusing on a complete working tool. 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? 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.