Mikhail R. Gadelha

Professional headshot of Mikhail R. Gadelha

Software Engineer at Igalia.

Phd in Computer Science [Thesis].

Projects

About me

I'm a Software Engineer at Igalia with a PhD in Computer Science and over 10 years of experience building systems. My work focuses on program verification, compilers, and static analysis. I'm a committer to LLVM and WebKit, and actively contribute to projects like ESBMC, CBMC, and Z3.

Recently, I've been focusing on RISC-V architecture optimization and serving as the maintainer of LLVM's libc RISC-V port.

I still write research papers in my free time and maintain an active interest in formal methods. My goal is to make robust verification tools and compiler optimizations accessible to developers building reliable, high-performance software.

GitHub Contributions

Loading the contribution calendar...

Publications

Talks, Technical Writing & Industry Impact

Boosting RISC-V Application Performance: An 8-Month LLVM Journey
Igalia Compilers Blog, May 2025
Chronicles an 8-month optimization effort that delivered significant performance improvements for RISC-V applications in LLVM. It details enhanced code generation strategies, libc optimizations, and maintainership of the RISC-V libc port. Work resulted in measurable performance gains across multiple benchmark suites.

RISC-V Support into LLVM's libc: Challenges and Solutions for 32-bit and 64-bit [Slides]
LLVM Developers' Meeting, October 2024
Technical presentation detailing the implementation of RISC-V support in LLVM's libc project. Addresses unique challenges in supporting both 32-bit and 64-bit RISC-V architectures, including ABI compatibility, syscall interfaces, and performance optimizations. As the RISC-V libc maintainer, presents architectural decisions and solutions for bringing full C library support to RISC-V platforms.

Recent Publications

ESBMC v7.7: Efficient Concurrent Software Verification with Scheduling, Incremental SMT and Partial Order Reduction
Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2025
Improves verification of concurrent C programs through dynamic thread scheduling, incremental SMT solving, and enhanced partial order reduction algorithms. Significantly reduces exploration of redundant states and enables faster bug detection in multi-threaded applications.

ESBMC v7.6: Enhanced model checking of C++ programs with clang AST
Science of Computer Programming, 2025
Introduces advanced C++ support through Clang AST integration, enabling comprehensive verification of modern C++ features including templates, lambda expressions, and STL containers. Demonstrates significant improvements in verification accuracy and coverage.

ESBMC v7.4: Harnessing the Power of Intervals
Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2024
Implements interval analysis techniques to improve precision in numeric computations and reduce false positives in verification. Enhances handling of floating-point arithmetic and improves scalability for complex numerical programs.

Open Source Contributions

LLVM/Clang - As a committer to the LLVM project, I've contributed to Clang compiler optimizations, the Clang Static Analyzer, and various tooling enhancements. Currently serving as maintainer of the RISC-V libc port, my recent focus has been on RISC-V code generation improvements and performance optimizations that have delivered significant gains for RISC-V applications.

WebKit - As a committer, I've contributed bug fixes, performance improvements, and new features to this critical web browser engine. My work helped ensure the stability and performance of web browsing for millions of users across Safari and other WebKit-based applications.

ESBMC - As a core contributor and maintainer, I've led the development of several key features including interval analysis, incremental SMT solving, and enhanced C++ support through Clang AST integration. My work has significantly improved verification performance and expanded the tool's capabilities for concurrent software verification.

CBMC - Contributed bug fixes and enhancements to this widely-used bounded model checker. My contributions focus on improving verification accuracy and extending language support for modern C++ features.

DSVerifier - Contributed to the development of this specialized verification tool for digital systems, helping to implement verification techniques for fixed-point arithmetic and finite word length effects in digital signal processing applications.

Z3 - Contributed bug fixes and improvements to this industry-standard SMT solver, which serves as a critical backend for many verification tools including ESBMC and CBMC.