I’ve posted an introduction on Pintool and one on Z3 on the blog of our CTF Team, De Eindbazen.

And, yes, these actually provided us with results!

Pintool Introduction: http://eindbazen.net/2013/04/pctf-2013-hypercomputer-1-bin-100/

Z3 Introduction: http://eindbazen.net/2013/04/pctf-2013-cone-binary-250-2/

Cheers,

Jurriaan

what is z3?

Thanks.

Sorry for the late reply. Z3 is a “high-performance theorem prover being developed at Microsoft Research.” It is useful for solving equations, such as as simple ones like “x+y = 42, if y = 1337, what is x?”, but also more advanced ones..

See also: http://z3.codeplex.com/