SE 504 (Formal Methods and Models)
Spring 2026

Syllabus

Homework Assignments

• Homework #1: A Couple Dafny Problems
• Homework #2: Proofs of Simple Programs
• Homework #3: Calculating wp in some Dafny Methods
• Homework #4: Proving Lemmata in Dafny
• Homework #5: Pencil-and-Paper Program Correctness Proofs
• Homework #6: Strengthen the Invariant; Tail Recursion

Programming Assignments

• None yet.

Dafny

• The Dafny Programming and Verification Language (home page)
• Getting Started with Dafny: A Guide (web page)
• Getting Started with Dafny: A Guide (original paper?)
• Dafny Reference Manual

Electronic Handouts

From SE 500:
• Gries/Schneider Theorems as presented by Warford
• On Proofs Involving the Replacement of A by B, where A implies B
• Developing Predicates from Informal Statements: A Checklist
• On the Strength/Weakness Relationship between Predicates
• Axioms for the (family of) if functions

New to SE 504:
• Properties/Laws of Hoare triples and the wp Predicate Transformer
• Law of Assumptions and Textual Substitution
• Program Verification Summary
• Correctness proofs of some simple programs:
  • A skip command
  • An assignment command   Another one
  • Calculating the right-hand side of an assignment command
  • Proof of Correctness of an If-Else Command
• Repetition (Looping)
  • Notes on Loop Invariants
  • Correctness proof of a program that computes 1+2+...+n
  • Development of a linear search program
  • Strengthening the Loop Invariant:
    • Development of a program to calculate Fibonacci numbers
    • Development of a program to compute N³ without multiplication or exponentation
    • Development of a program that does negative-positive pair counting in an array
    • Development of a program for the Maximum Segment Sum Problem
• Tail Recursion
  • Developing programs to compute tail recursive functions

External Links

• The Correctness-by-Construction Approach to Programming, by D.G. Kourie and Bruce W. Watson.
• Wikipedia entry on Design by Contract

Work by Bertrand Meyer on Program Correctness

• Bertrand Meyer's technology+ blog
• Loop invariants: analysis, classification, and examples
• Links to Publications
• Applying "Design by Contract"
• A Framework for Proving Contract-equipped Classes
• Towards Practical Proofs of Class Correctness
• Proving Pointer Program Properties Part 1: Context and Overview
• Proving Pointer Program Properties Part 2: The Overall Object Structure