SMT for DSLs: a Tutorial

Cody Roux gives an overview of the sbv library for interacting with SMT solvers in Haskell, and gives strategies for using it to verify properties of/in domain specific languages.