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/