The goal of my RECON 2012 keynote speech was to introduce methods in academic program analysis and demonstrate -- intuitively, without drawing too much on formalism -- how they can be used to solve practical problems that are interesting to industrial researchers in the real world. Given that it was the keynote speech, and my goal of making the material as accessible as possible, I attempted to make my points with pictures instead of dense technical explanations. As a result, one might consider this presentation to be a friendly (but decidedly incomplete) introduction to binary program analysis as opposed to a rigorous mathematical monograph. The presentation features five detailed expositions of applying static program analysis (abstract interpretation and SMT solving) towards practically-interesting reverse engineering problems. (Aside: it's quite challenging to present this material without using terms such as "lattice", "Galois connection", etc.!)
Unfortunately, due to an error with the camera, the recording of the talk does not exist. This is problematic: I failed somewhat in walking the sharp edge of Einstein's razor, "as simple as possible, but no simpler" -- it was in fact made simpler than what was possible, and some important details (for example, about relational abstract interpretation and reduced products) were included in the spoken material but not the actual slides. Therefore, the learned reader is advised to imagine judiciously-placed asterisks and the accompanying errata, and the untutored pupil would be well-advised to recognize the incomplete and intuitive nature of the exposition and perhaps consult this program analysis reading list. I would like to give the talk at some other conference at which the video can be reliably recorded, so that it may be published online.
Here are the slides.