I have been meaning to learn about SMT based program analysis for a long time and recently I started learning about the topic. There are so many frameworks, articles and tutorials out there that I shall explore as time goes by.

Since I am still learning, I do not claim that the following material is rocket science or advanced by any means, instead, it is very basic and should be approachable enough by absolute beginners to Z3 (a theorem prover from Microsoft Research). All I know so far comes from reading Dennis Yurichev‘s e-book “Quick introduction into SAT/SMT solvers and symbolic execution” in addition to the Z3Py introductory material by Eric (https://github.com/ericpony/z3py-tutorial).

In last week’s blog post, I illustrated how to write a basic emulator to evaluate a function’s return value without running it. In today’s blog post, I am going to show how to convert thousands of arithmetic operations from x86 assembly code into simplified Z3 expressions. Continue reading →