Mikhail Y. R. Gadelha

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