This pop-scientific conference paper introduces Mythril, a security analysis tool for Ethereum smart contracts, and its symbolic execution backend LASER-Ethereum. The first part of the paper explains symbolic execution of Ethereum bytecode in a largely formal manner. The second part showcases the vulnerability detection modules already implemented in Mythril. The modules use a pragmatic mix of static analysis, symbolic analysis and control flow checking.
You can download it from the following link: https://packetstormsecurity.com/files/download/147201/smashing-smart-contracts-1of1.pdf
Source: https://packetstormsecurity.com/files/147201/Smashing-Smart-Contracts.html