Jump to content
Tuts 4 You

Keygenning Using the Z3 SMT Solver

Teddy Rogers

About This File

Quoting Wikipedia, In computer science and mathematical logic, the satisfiability modulo theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first order logic with equality. Formally speaking, an SMT instance is a formula in first order logic, where some function and predicate symbols have additional interpretations, and SMT is the problem of determining whether such a formula is satisfiable.

This article shows how we can use an SMT solver in developing a key generator. We need to find valid keys while also satisfying certain constraints. We will use the Z3 SMT Solver, as it is quite easy to use and also has a nice python API to code against.

User Feedback

Recommended Comments

There are no comments to display.

Create an account or sign in to comment

You need to be a member in order to leave a comment

Create an account

Sign up for a new account in our community. It's easy!

Register a new account

Sign in

Already have an account? Sign in here.

Sign In Now
  • Create New...