Concrete and Abstract Interpretation, Explained through Chess

I've decided to release my presentation (two slide decks) on the theoretical foundations of abstract interpretation, illustrated through the game of chess. It has been collecting dust on my hard drive for five years, so I figured I may as well give it a proper burial.

This was the first thing I wrote as part of what eventually became my SMT-Based Program Analysis training, back when I planned for that course to cover abstract interpretation as well as logical analysis. The idea to use chess as a medium came to me in a nightmare. I spent about six weeks working on it, polishing it, and extending my original ideas to cover broader areas of abstract interpretation than what my nightmare originally entailed. Writing it was a useful exercise; it forced me to muddle through all of the formalism you see in the preliminaries section of an abstract interpretation paper, and digest them well enough that I thought I could present them to other people. And I personally liked what I wrote, especially the detailed figures.

Next, I sent it off to proofreaders. Two of them -- people with graduate degrees in program analysis and mathematics -- also liked it. The other 18 or so of them -- bright people, mostly professional security researchers -- seemed to utterly despise it. I think they were angry at me for sending it to them with a straight face and expecting a response. You know who you are, and I'm sorry for putting you through that. There were some more changes I wanted to make, but the response made me finally realize that you need at least an undergraduate education in mathematics to understand abstract interpretation, no matter how hard I might try to make it friendly. The experience ultimately convinced me that my time was better spent in teaching people about SMT solvers.

Now it's my turn to preemptively offer my apologies, and best wishes for luck, to anybody else who would like to read this. Chances are very good that you are not going to like it, either. The second deck could use some more polishing, but that's the least of your worries. The bigger problem is that the audience for this document is virtually non-existent.

After that compelling interlude, I present:

P.S. if you find any corrections, don't bother sending them since I have no intention of working on this anymore.

Bonus picture, a preview of what awaits you.

ai-lobster.png