COMP 590-205 — Formal Methods: Syllabus Draft

Spring 2027 — planning draft. Topics, tools, and assessment details remain tentative.

Course Description

How do we build evidence that software behaves as intended? This course takes a practical approach to formal methods by placing them within the broader spectrum of testing and verification. We begin with testing and modern development workflows, then explore increasingly systematic approaches to analyzing behavior and checking properties, culminating in deductive verification and machine-checked proofs.

Students will use tools, write specifications, reproduce failures, and interpret results. Throughout the course, we will ask what each technique establishes, what assumptions it relies on, and how its guarantees compare with its cost and scalability. The primary focus is software; selected hardware examples may illustrate connections across domains.

Learning Goals

By the end of the course, students should be able to:

Explain and compare techniques across the spectrum from testing and fuzzing to model checking and machine-checked proofs.
Select a verification strategy based on system requirements, desired guarantees, scalability, and cost.
Design and use testing and verification workflows that combine regression tests, continuous integration, automated test generation, and analysis tools.
Apply contemporary tools to detect bugs, check properties, and analyze software behavior, with possible extensions to hardware examples.
Write and evaluate specifications, assertions, and invariants, and interpret evidence such as coverage, counterexamples, execution traces, and proofs.
Communicate the assumptions and limitations of a verification claim, including the distinction between checking an implementation and choosing the right specification.

Tentative Topics and Sequence

The following is a proposed progression, not a commitment to cover every subtopic.

1. Correctness and Testing Workflows

Verification versus validation; requirements and specifications; bugs, failures, and specification errors. Unit, integration, and system testing; test oracles; coverage; regression suites; automated builds and CI checks. What should prevent code from merging or shipping?

2. Test Generation, Fuzzing, and Dynamic Analysis

Boundary cases and property-based testing; AI-assisted test generation and evaluating generated tests; selected differential or metamorphic testing examples. Coverage-guided fuzzing, seeds, crash minimization, runtime assertions, and sanitizers. What does finding no failures tell us?

3. Static Analysis and Precise Properties

Compiler checks, dataflow and taint analysis, and conceptual foundations of static analysis. False positives and negatives, soundness, and completeness. Preconditions, postconditions, contracts, invariants, and safety versus liveness properties.

4. Symbolic Execution and Model Checking

Symbolic inputs, path constraints, SAT/SMT queries, and counterexamples. State-space exploration, reachability, and bounded model checking. Path and state explosion, modeling choices, and the limits of bounded results.

5. Deductive Verification and Machine-Checked Proofs

Practical program reasoning with contracts and loop invariants; verification conditions and automation. An introduction to interactive proof assistants, proof generation versus proof checking, and trusted computing bases. Selected verified-system case studies may connect these ideas to larger implementations.

Optional Hardware Connections

Depending on time, examples may include simulation and testbenches, hardware assertions, or formal property and equivalence checking. These will complement the software emphasis.

Materials and Tools

The planned rhythm is to try a tool roughly every one to two weeks. Candidates include:

Area	Candidate tools
Testing and CI	pytest or JUnit; GitHub Actions
Property-based testing	Hypothesis or QuickCheck
Fuzzing and runtime checking	AFL/libFuzzer; Clang sanitizers
Static analysis	CodeQL
Constraint solving	Z3
Symbolic execution and bounded checking	KLEE; CBMC
Deductive verification	Dafny
Interactive proofs and proof checking	Lean or Rocq
Optional hardware verification	SystemVerilog Assertions and a suitable formal tool

This is a candidate list, not a required installation list. Final choices, readings, and setup instructions will be announced before they are needed.

Coursework and Assessment

Planned work combines practical tool exercises, short written explanations, and in-class discussion. Students will be expected to explain their specifications, interpret tool output, and evaluate what their results support—not simply report that a tool passed or failed.

Grading weights, assignment counts, deadlines, and any exam requirements are TBA.

Proposed Final Project: Compare Verification Approaches

Choose an open-source codebase and apply multiple tools from different parts of the verification spectrum. Define the behavior or properties you want to investigate, then compare what each approach could and could not establish.

The comparison should address:

The properties checked and how they were expressed.
Bugs, counterexamples, or other evidence produced by each tool.
Assumptions, bounds, and limitations of the results.
Setup effort, runtime, scalability, and usefulness for the chosen codebase.
Which combination of techniques you would recommend and why.

The goal is an evidence-based comparison, including an explanation of why passing tests or receiving a successful verification result does not automatically establish every desired property. Project scope, team size, milestones, and deliverables will be finalized later.

Prerequisites and Preparation

Official prerequisites and recommended background: TBA.

Course Policies

Attendance, collaboration, permitted AI use, academic integrity, late work, accommodations, and other course policies will be added before the semester begins. Studying AI-generated tests does not by itself establish a policy permitting AI use on assignments.

Logistics

Meeting times, location, office hours, course staff, and important dates: TBA.