8.17

Notes🔗

These are the course notes for CMSC 433. If you notice any errors, unclear explanations, missing content, or have suggestions for improvement, please submit an issue on Github or email anwar@umd.edu.

    1 Dafny Cheatsheet

    2 Dafny Basics

    3 Getting Started with Dafny

    4 Dafny Collections

    5 Floyd Hoare Logic

    6 Inductive Proofs

    7 Inductive Types

    8 Sorting

    9 Loop Invariants

    10 Arrays

    11 SAT Solvers

    12 Solving SAT and SMT Problems Using Z3

    13 Symbolic Execution

    14 Testing

    15 Functional Programming in Rocq

    16 Logic in Rocq

    17 Induction in Rocq