For both SW and HW hacking, SAT and SMT solvers and their associated toolchains could be used to automate a lot of boring tasks for you, getting you to the next stage of that exploit chain you have been working on, or just helping you make sure there are no exploitable bugs in your soft- or hardware. In this talk I will go into what SAT and SMT solvers are, what kind of solvers are out there and give some practical examples in using them both to find, e.g. crack codes or bugs in systems. In particular, I will showcase some interesting use-cases of SAT solvers for cryptography, SMT solvers for puzzle-solving, and concolic execution (using SMT solvers) for automated bug-finding.

Mate Soos has been developing the CryptoMiniSat SAT solver for over 7 years that has is used in many places both in academia and industry and he helps maintain the SMT solver STP that is widely used in both industry and research.