Modern processors are more prone to errors than ever due to rapid scaling of technology. It is no longer practical to simply ensure fully reliable execution and, in addition, programs gain efficiency by allowing occasional errors. Developers can leverage faulty hardware to increase the efficiency of their programs, but also need to verify the safety of their programs. The verification system Leto gives developers the ability to specify and verify the correctness of assertions relating the reliable and relaxed semantics of their program. This project aims to build an interpreter for Leto, allowing developers to run their programs under a simulation of faulty conditions, letting them empirically verify the safety of their programs.

I am participating in SuperUROP to gain research experience and see whether I’ m interested in doing a PhD and pursuing a career in research. This past summer, I worked on a research and development team at Siemens Healthineers. I hope to learn more about the research process since I’ m not very familiar with it, and I hope to learn whether I enjoy it. I think the project has many exciting practical applications.