Proposal of a cryptography method using gray scale digital images. - Mikhail Y. R. Gadelha; Cicero Ferreira Fernandes Costa Filho; Marly Guimarães Fernandes Costa (ICITST, 2012)

Bounded model checking for fixed-point digital filters. - Renato B. Abreu; Mikhail Y. R. Gadelha; Lucas C. Cordeiro; Eddie Batista de Lima Filho; Waldir S. S. Júnior (J. Braz. Comput. Soc., 2016)

Encoding Floating-Point Numbers Using the SMT Theory in ESBMC: An Empirical Evaluation over the SV-COMP Benchmarks. - Mikhail Y. R. Gadelha; Lucas C. Cordeiro; Denis A. Nicole (SBMF, 2017)

Counterexample-Guided k-Induction Verification for Fast Bug Detection. - Mikhail Y. R. Gadelha; Lucas C. Cordeiro; Denis A. Nicole (CoRR, 2017)

Handling loops in bounded model checking of C programs via k-induction. - Mikhail Y. R. Gadelha; Hussama Ibrahim Ismail; Lucas C. Cordeiro (Int. J. Softw. Tools Technol. Transf., 2017)

ESBMC 5.0: an industrial-strength C model checker. - Mikhail Y. R. Gadelha; Felipe R. Monteiro; Jeremy Morse; Lucas C. Cordeiro; Bernd Fischer 002; Denis A. Nicole (ASE, 2018)

Towards counterexample-guided k-induction for fast bug detection. - Mikhail Y. R. Gadelha; Felipe R. Monteiro; Lucas C. Cordeiro; Denis A. Nicole (ESEC/SIGSOFT FSE, 2018)

Themes Validation Tool. - Everlandio Fernandes; Rodrigo Correia; Adriano Gil; Juliana Postal; Mikhail R. Gadelha (HCI (37), 2019)

A Robust and Real-Time Face Anti-spoofing Method Based on Texture Feature Analysis. - Aasim Khurshid; Sergio Cleger Tamayo; Everlandio Fernandes; Mikhail R. Gadelha; Mauro Teófilo (HCI (LBP), 2019)

SMT-based refutation of spurious bug reports in the clang static analyzer. - Mikhail Y. R. Gadelha; Enrico Steffinlongo; Lucas C. Cordeiro; Bernd Fischer 002; Denis A. Nicole (ICSE (Companion Volume), 2019)

Incremental Bounded Model Checking of Artificial Neural Networks in CUDA. - Luiz H. Sena; Iury Valente de Bessa; Mikhail Y. R. Gadelha; Lucas C. Cordeiro; Edjard Mota (SBESC, 2019)

ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference - (Competition Contribution). - Mikhail Y. R. Gadelha; Felipe R. Monteiro; Lucas C. Cordeiro; Denis A. Nicole (TACAS (3), 2019)

Beyond k-induction: Learning from Counterexamples to Bidirectionally Explore the State Space. - Mikhail Y. R. Gadelha; Felipe R. Monteiro; Enrico Steffinlongo; Lucas C. Cordeiro; Denis A. Nicole (CoRR, 2019)

Boost the Impact of Continuous Formal Verification in Industry. - Felipe R. Monteiro; Mikhail Y. R. Gadelha; Lucas C. Cordeiro (CoRR, 2019)

Scalable and precise verification based on k-induction, symbolic execution and floating-point theory. - Mikhail Y. R. Gadelha (2019)

Experimental Data for Model Checking C++03 Programs. - Felipe R. Monteiro; Mikhail R. Gadelha; Lucas C. Cordeiro (IEEE DataPort, 2019)

ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory - (Competition Contribution). - Mikhail Y. R. Gadelha; Rafael Menezes; Felipe R. Monteiro; Lucas C. Cordeiro; Denis A. Nicole (FASE, 2020)

Automatic Contrast Evaluation for Android Themes. - Adriano Gil; Juliana Postal; Adélia Ferreira; Daydlene Gonçalves; Bianca Hayek Bianco; Mikhail R. Gadelha (HCI (44), 2020)

An Efficient Floating-Point Bit-Blasting API for Verifying C Programs. - Mikhail R. Gadelha; Lucas C. Cordeiro; Denis A. Nicole (VSTTE, 2020)

FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs. - Kaled M. Alshmrany; Rafael S. Menezes; Mikhail R. Gadelha; Lucas C. Cordeiro (CoRR, 2020)

FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs (Competition Contribution). - Kaled M. Alshmrany; Rafael S. Menezes; Mikhail R. Gadelha; Lucas C. Cordeiro (FASE, 2021)

Visual Prediction Based on Photorealistic Style Transfer. - Everlandio Fernandes; Everton Lima Aleixo; Wesley Jacinto Barreira; Mikhail R. Gadelha; Aasim Khurshid; Sergio Cleger Tamayo (HCI (36), 2021)

Software Usability Evaluation for Augmented Reality Through User Tests. - Guto Kawakami; Aasim Khurshid; Mikhail R. Gadelha (HCI (44), 2021)

Verification and refutation of C programs based on k-induction and invariant inference. - Omar M. Alhawi; Herbert Rocha; Mikhail R. Gadelha; Lucas C. Cordeiro; Eddie Batista de Lima Filho (Int. J. Softw. Tools Technol. Transf., 2021)

ESBMC 6.1: automated test case generation using bounded model checking. - Mikhail R. Gadelha; Rafael S. Menezes; Lucas C. Cordeiro (Int. J. Softw. Tools Technol. Transf., 2021)

Summary of Model Checking C++ Programs. - Felipe R. Monteiro; Mikhail R. Gadelha; Lucas C. Cordeiro (ICST, 2022)

ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC. - Franz Brauße; Fedor Shmarov; Rafael Menezes; Mikhail R. Gadelha; Konstantin Korovin; Giles Reger; Lucas C. Cordeiro (ISSTA, 2022)

Model checking C++ programs. - Felipe R. Monteiro; Mikhail R. Gadelha; Lucas C. Cordeiro (Softw. Test. Verification Reliab., 2022)

FuSeBMC v.5: Interval Analysis and Methods for Test Case Generation. - Mohannad Aldughaim; Kaled M. Alshmrany; Mikhail R. Gadelha; Rosiane de Freitas; Lucas C. Cordeiro (Zenodo, 2022)

FuSeBMC_IA: Interval Analysis and Methods for Test Case Generation - (Competition Contribution). - Mohannad Aldughaim; Kaled M. Alshmrany; Mikhail R. Gadelha; Rosiane de Freitas; Lucas C. Cordeiro (FASE, 2023)

ESBMC v7.3: Model Checking C++ Programs Using Clang AST. - Kunjian Song; Mikhail R. Gadelha; Franz Brauße; Rafael S. Menezes; Lucas C. Cordeiro (SBMF, 2023)

ESBMC v7.4: Harnessing the Power of Intervals. - Rafael Menezes; Mohannad Aldughaim; Bruno Farias 001; Xianzhiyu Li; Edoardo Manino; Fedor Shmarov; Kunjian Song; Franz Brauße; Mikhail R. Gadelha; Norbert Tihanyi; Konstantin Korovin; Lucas C. Cordeiro (CoRR, 2023)

ESBMC v7.4: Harnessing the Power of Intervals - (Competition Contribution). - Rafael Sá Menezes; Mohannad Aldughaim; Bruno Farias 001; Xianzhiyu Li; Edoardo Manino; Fedor Shmarov; Kunjian Song; Franz Brauße; Mikhail R. Gadelha; Norbert Tihanyi; Konstantin Korovin; Lucas C. Cordeiro (TACAS (3), 2024)

ESBMC v7.7: Efficient Concurrent Software Verification with Scheduling, Incremental SMT and Partial Order Reduction - (Competition Contribution). - Tong Wu; Xianzhiyu Li; Edoardo Manino; Rafael Sá Menezes; Mikhail R. Gadelha; Shale Xiong; Norbert Tihanyi; Pavlos Petoumenos; Lucas C. Cordeiro (TACAS (3), 2025)

ESBMC v7.6: Enhanced model checking of C++ programs with clang AST. - Xianzhiyu Li; Kunjian Song; Mikhail R. Gadelha; Franz Brauße; Rafael S. Menezes; Konstantin Korovin; Lucas C. Cordeiro (Sci. Comput. Program., 2025)