About the same time I wrote the aforementioned interpreter, I also was interested in the more mathy side of computer science. A fantastic mentor I had was deeply entrenched in reversing and got me involved in the applications of math to the more practical side of thing. In my quest to improve my mathematical ability I wrote this paper on model checking. More interesting, could model checking be one day used for automated vulnerability analysis? Food for thought, but for now computational power falls short. NP completeness is a bitch :-(. I wrote the paper to be an introduction to the topic so it might be a bit more beginner friendly.