Sidney Amani, Myriam Bégel, Maksym Bortin, Mark Staples: Towards verifying ethereum smart contract bytecode in Isabelle/HOL. CPP 2018: 66-77