Mikhail Y. R. Gadelha

Publication Activity (10 Years)

Years Active: 2012-2020
Publications (10 Years): 15

Top Topics

Floating Point Arithmetic

Digital Filters

Bounded Model Checking

Top Venues

ICSE (Companion Volume)

Int. J. Softw. Tools Technol. Transf.

Publications

Mikhail Y. R. Gadelha, Lucas C. Cordeiro, Denis A. Nicole
An Efficient Floating-Point Bit-Blasting API for Verifying C Programs. CoRR (2020)
Mikhail Y. R. Gadelha, Rafael Menezes, Felipe R. Monteiro, Lucas C. Cordeiro, Denis A. Nicole
ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory - (Competition Contribution). FASE (2020)
Luiz H. Sena, Iury Valente de Bessa, Mikhail Y. R. Gadelha, Lucas C. Cordeiro, Edjard Mota
Incremental Bounded Model Checking of Artificial Neural Networks in CUDA. SBESC (2019)
Luiz H. Sena, Iury Valente de Bessa, Mikhail Y. R. Gadelha, Lucas C. Cordeiro, Edjard Mota
Incremental Bounded Model Checking of Artificial Neural Networks in CUDA. CoRR (2019)
Mikhail Y. R. Gadelha, Felipe R. Monteiro, Lucas C. Cordeiro, Denis A. Nicole
ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference - (Competition Contribution). TACAS (3) (2019)
Mikhail Y. R. Gadelha, Felipe R. Monteiro, Enrico Steffinlongo, Lucas C. Cordeiro, Denis A. Nicole
Beyond k-induction: Learning from Counterexamples to Bidirectionally Explore the State Space. CoRR (2019)
Felipe R. Monteiro, Mikhail Y. R. Gadelha, Lucas C. Cordeiro
Boost the Impact of Continuous Formal Verification in Industry. CoRR (2019)
Mikhail Y. R. Gadelha, Enrico Steffinlongo, Lucas C. Cordeiro, Bernd Fischer, Denis A. Nicole
SMT-based refutation of spurious bug reports in the clang static analyzer. ICSE (Companion Volume) (2019)
Mikhail Y. R. Gadelha, Enrico Steffinlongo, Lucas C. Cordeiro, Bernd Fischer, Denis A. Nicole
SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer. CoRR (2018)
Mikhail Y. R. Gadelha, Felipe R. Monteiro, Jeremy Morse, Lucas C. Cordeiro, Bernd Fischer, Denis A. Nicole
ESBMC 5.0: an industrial-strength C model checker. ASE (2018)
Mikhail Y. R. Gadelha, Felipe R. Monteiro, Lucas C. Cordeiro, Denis A. Nicole
Towards counterexample-guided k-induction for fast bug detection. ESEC/SIGSOFT FSE (2018)
Mikhail Y. R. Gadelha, Lucas C. Cordeiro, Denis A. Nicole
Encoding Floating-Point Numbers Using the SMT Theory in ESBMC: An Empirical Evaluation over the SV-COMP Benchmarks. SBMF (2017)
Mikhail Y. R. Gadelha, Lucas C. Cordeiro, Denis A. Nicole
Counterexample-Guided k-Induction Verification for Fast Bug Detection. CoRR (2017)
Mikhail Y. R. Gadelha, Hussama Ibrahim Ismail, Lucas C. Cordeiro
Handling loops in bounded model checking of C programs via k-induction. Int. J. Softw. Tools Technol. Transf. 19 (1) (2017)
Renato B. Abreu, Mikhail Y. R. Gadelha, Lucas C. Cordeiro, Eddie Batista de Lima Filho, Waldir Sabino da Silva Jr.
Bounded model checking for fixed-point digital filters. J. Braz. Comput. Soc. 22 (1) (2016)
Mikhail Y. R. Gadelha, Cicero Ferreira Fernandes Costa Filho, Marly Guimarães Fernandes Costa
Proposal of a cryptography method using gray scale digital images. ICITST (2012)