Final Project Guide

Purpose

The course introduces several approaches to formal verification, but it cannot explore every technique or application in depth. The final project is an opportunity to choose one focused question that interests you and investigate it more deeply through both reading and technical work.

By the end of the project, you should understand your chosen question well enough to explain the relevant ideas, apply them to an interesting problem, and assess what worked, what did not, and why.

Expected scope

This is a course project, not an expectation that you produce publication-ready research. A focused, carefully executed project with a modest contribution is preferable to an ambitious project that never reaches a meaningful result.

Every project should include:

• enough reading to understand and situate the work;
• a clear question, goal, or claim;
• a substantive technical component, such as implementation, formalization, experimentation, replication, comparison, or case-study investigation; and
• evidence and analysis that support the conclusions.

The exact balance will depend on the project. You are not required to build a large tool or prove a new theorem.

What counts as a contribution?

Projects should go beyond simply following a tutorial or reproducing a worked example unchanged. The contribution can be modest. Suitable forms include:

• applying a verification technique to a new program, algorithm, or domain;
• replicating a published result and carefully analyzing agreements, discrepancies, or limitations;
• comparing two encodings, tools, proof strategies, or verification methods;
• extending an existing example, benchmark, or tool in a meaningful way;
• developing a small prototype that investigates a specific research idea;
• formalizing and proving a result that is not already supplied as a course exercise; or
• conducting a systematic investigation that produces a useful negative result.

Novelty here does not mean inventing an entirely new research area. A new application, careful comparison, useful extension, or well-analyzed replication can be enough. A negative result is also valuable when the question and method are sound and the limitations are explained honestly.

There is no archive of projects from earlier offerings of this course. Use the forms above to judge an appropriate scope, and discuss uncertain ideas with the instructor early.

Teams

Projects should normally be completed in teams of two or three. Small teams bring together a useful mix of skills, support shared problem solving, and make the project workload more manageable.

A one-person team is permitted only with prior instructor approval. The student must demonstrate a clear, feasible plan and sufficient preparation to carry out the proposed work independently—in other words, you should choose this option only if you know what you are doing.

Every team member must make a substantive contribution and understand the project as a whole. The team should divide work explicitly, communicate regularly, and raise collaboration problems early.

A project may overlap with ongoing research, another course, or work by someone outside this class only with prior instructor approval. Any overlap must be disclosed in the proposal, and the work being submitted for CMPUT 664 must be clearly identified.

Project proposal

Each team will submit a short written proposal. It should:

• list the team members;
• state the problem or research question;
• explain why the question is relevant to formal verification;
• identify and cite the most relevant prior work;
• describe the intended technical approach and how it will be evaluated; and
• give concrete intermediate milestones, including a minimum viable result and any stretch goals.

A plan that permits partial progress is essential. Avoid an all-or-nothing project whose value depends on one final experiment or proof succeeding. Proposals may be returned for revision so that the scope and evaluation plan are clear and feasible.

Presentation

Each team will present its work during the scheduled presentation sessions. The presentation should communicate the motivation, approach, most important results, limitations, and possible next steps. All team members must participate and should be able to answer questions about the project as a whole.

The talk length and presentation order will be announced after teams are formed.

Final report

Each team will submit a concise research-style report that explains the problem, relevant prior work, approach, results, limitations, and conclusions. The report should make clear what the team built, proved, evaluated, or learned and should distinguish evidence from speculation. Detailed length, formatting, and submission requirements will be announced with the report assignment.

How the project will be assessed

The project will be evaluated as a whole, with attention to:

• the clarity and relevance of the question;
• technical correctness and depth appropriate to the course;
• the quality of the implementation, formalization, experiments, or investigation;
• use and understanding of related work;
• the quality of evidence and analysis, including treatment of limitations;
• the presentation and final report; and
• each team member’s contribution and understanding.

Please note that a smaller project executed and analyzed carefully can be stronger than a larger but incomplete one.

Getting feedback

Successful projects require initiative, but you are not expected to design the project in isolation. Discuss ideas with potential teammates and seek feedback from the instructor before investing heavily in an approach. Continue asking for feedback when the scope, method, or evaluation is uncertain.