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
Publications
Talks, Technical Writing & Industry Impact
Unlocking 15% More Performance: A Case Study in LLVM Optimization for RISC-V
[Slides][Blog post]
RISC-V North America Summit, October 2025
Technical presentation into optimizing LLVM for RISC-V architecture, showcasing real-world performance improvements. Presents a comprehensive case study demonstrating how systematic compiler optimizations, code generation improvements, and targeted enhancements to LLVM's RISC-V backend can unlock significant performance gains.
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 [PDF]
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 [PDF]
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 [PDF]
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 [Contributions]
As a committer to the LLVM project and maintainer of the RISC-V libc port, I focus on backend code generation and performance. My recent work includes extensive updates to the SpacemiT-X60 scheduling model using hardware-measured latencies and significant contributions to the RISC-V VLOptimizer (VLOPT). I also work on enhancing cost models and enabling new libc functionality for the architecture.
WebKit [Contributions]
As a committer, I've contributed bug fixes, performance improvements, and new features to JavaScriptCore (JSC), WebKit's JavaScript engine. My recent work focuses on the BBQ JIT, specifically bringing WebAssembly SIMD support to 32-bit architectures (ARMv7) and optimizing code generation for shifts, rotates, and several 64-bit operations, resulting in significant code size reductions and performance gains.
ESBMC [Contributions]
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.