Z3 is a powerful theorem prover/SMT solver developed by Microsoft. We will use it to break hash functions, pseudo-random number generators, and more.

Have you ever tried spinning a tennis racket? It's pretty easy to spin one along the axis of the handle, and it's also not that hard to spin it around an axis perpendicular to the plane of the racket, but try spinning it "end over end" about the third axis (in the plane of the racket, perpendicular to the handle) and you'll find that the racket always seems to flip over and start rotating about other axes as it spins. In this class we'll prove mathematically why this is is true, and in the process we'll learn about Euler's equations, the moment of inertia tensor, and more!

If you've ever taken a calculus course, you know that integration acts a lot like a sum. We have a lot of rules and theorems for dealing with integrals, so can we transfer some of them over to help us deal with sums? In this class we'll define discrete analogs for the derivative and the integral, and in the process we'll learn about the discrete product rule, the fundamental theorem of discrete calculus, and the discrete version of the number e.