Reading and Core concepts Symbolic Execution my playlist Satisfiability modulo theories Conjunctive normal form Algebra: Systems of linear inequalities MIT - OpenCourse: Symbolic Execution - VIDEO Felipe Manzano & Josselin Feist - Automatic bugfinding for the blockchain Manticore Workshop - EthCC 2018 Examples Introduction examples using Manticore