We will explore how different formal methods like model checking and theorem proving can be used to certify the correctness of Xen's working. We will also discuss the different benefits of a verified kernel, especially for embedded systems, and the various certifications.
Student at EPITA, a French engineering school, specializing in security, networks, and industrial systems, with a particular interest in formal methods and kernel verification.