Mikhail R. Gadelha

about image

Software Engineer at Igalia.

Phd in Computer Science [Thesis].

Projects

About me

A recovering academic with 10+ years of experience in software development.
Open-source enthusiast.
Interested in C/C++ software development, program verification (model checking and static analysis), and compilers.
LLVM and Webkit committer.

Recent Publications

Summary of Model Checking C++ Programs. In ICST, 2022.
Model Checking C++ Programs. In Softw Test Verif Reliab, 2022.
ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC. In ISSTA, 2022.

GitHub Contributions

Loading github stats.

Open Source Contributions

ESBMC is a context-bounded model checker for embedded C/C++ software based on Satisfiability Modulo Theories (SMT) solver. It allows the verification engineer to verify single- and multi-threaded software (with shared variables and locks); to reason about arithmetic under- and overflow, pointer safety, memory leaks, array bounds, atomicity and order violations, deadlock and data race; to verify programs that make use of bit-level, pointers, structs, unions and fixed-point arithmetic.

CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, C99, most of C11 and most compiler extensions provided by gcc and Visual Studio.

DSVerifier (Digital Systems Verifier) is a bounded model checker to aid enginners to check for overflow, limit cycle, error, timing, stability, and minimum phase in digital systems, considering finite word length (FWL) effects.

WebKit is the web browser engine used by Safari, Mail, App Store, and many other apps on macOS, iOS, and Linux.

clang is language front-end and tooling infrastructure for languages in the C language family (C, C++, Objective C/C++, OpenCL, CUDA, and RenderScript) for the LLVM project.

Z3 is an SMT solver from Microsoft Research.