Rafael Sa Menezes

Rafael Sa Menezes is a Research Associate and Ph.D. student at the University of Manchester, specializing in Software Verification and Model Checking. His work focuses on applying formal verification techniques to industrial software systems, including Android applications, firmware, and optimizing verification processes through methods like fuzzing integration. He is a lead developer of ESBMC, a widely used open-source model checker for C and C++ programs. Rafael holds a Master of Science in Informatics from Universidade Federal do Amazonas (2021) and a Bachelor of Science in Computer Science from Federal University of Roraima (2017).

His research interests encompass static and dynamic analysis, concurrency verification, and improving the efficiency of verification tools through techniques such as global common subexpression elimination and control-flow graph instrumentation. Collaborations include advancements in branch coverage analysis and concurrent program verification via scheduling and partial order reduction methods.

Rafael’s contributions bridge academic research with practical industrial applications, addressing challenges in ensuring software reliability and security across diverse domains. His work has been presented at leading conferences including FSE and TACAS, with publications focusing on tool development and verification optimization strategies.