See also this paper: http://www.ieee-security.org/TC/SPW2014/papers/5103a198.PDF. The authors implement a pdf file format parser and find bugs in pretty much all of the existing implementations. Basically pdf is a pretty shitty file format with several ill-defined corner cases. This is one of the reasons PDFs tend to be vectors for security breaches.
The lead author (Andreas Bogk) presented an earlier version of this work at the Chaos Communication Camp in 2011 ("Certified Programming With Dependent Types").
I went to that talk, and found it to be probably the most advanced and difficult math lecture I'd ever attended! (I was very grateful to see such mathematical sophistication brought to bear to protect PDF users, which is almost all of us.)
