Abstract: This would be an introduction to SAT (Boolean Satisfiability) and SMT(Satisfiability Modulo Theories). It would then include how symbolic execution can be used to solve reverse engineering problems by modelling conditions as mathematical equations and constraints. This would be followed by a brief about how symbolic execution works and how code discovery is performed by a symbolic engine. This would be followed by 2 examples of solving a reverse engineering challenge using symbolic execution. The first method will demonstrate the use of the Z3 theorem prover from Microsoft Research. This would include modelling the conditions in the binary as boolean logic. The second example will demonstrate the use of angr which as another symbolic execution framework developed by the Computer Security Lab at UC Santa Barbara. This would be followed by a discussion on the shortcomings of symbolic execution and what steps can be taken to optimise the performance of a symbolic execution engine.