Labs I've written for classes:

    - sat-chaff: implement a basic DPLL SAT solver, profile it, then optimize
      it with the watched literals trick from Chaff

    - smt-symex: implement a bitblasting QF_ABV SMT solver and use it to build
      a symbolic execution engine (builds on sat-chaff)

    - static-analysis: implement a mini static analysis pass that finds some
      bugs in the Linux kernel

There are some "work-in-progress labs:"

    - neural-net: implement a simple feed-forward neural net training &
      inference program. the code is kind of a mess right now, but it's the
      smallest/simplest backprop implementation I know of. one of our 240lx
      students (Luca Pistor) even got it running on the pi.