miniblog.

← Back to all posts

Wilfred Hughes

Aug 3, 2017 at 08:01

Dynamically generating shellcode using an SMT solver: almost magical! https://sean.heelan.io/2009/06/01/fun-uses-for-an-smt-solver/

Fun uses for an SMT solver

Fun uses for an SMT solver

An SMT solver (such as Z3, Yices or STP) is a decision procedure that can handle various types of arithmetic and other decidable theories. They make use of procedures specific to the theories they …