Henrik Karlsson is a PhD student at the Secure and Trustworth Execution Platform research group at the Division of Theoretical Computer Science at KTH Royal Institute of Technology, Sweden. Henrik’s research focuses mainly on the design, modelling and verification of separation kernels for high-assurance systems, and the modelling and verification of multicore architectures and program binaries.