**Selected Papers**

- ESBMC v6.0: Verifying C Programs using k-Induction and Invariant Inference (Competition Contribution)
- ESBMC 5.0: An Industrial-Strength C Model Checker
- ESBMC-GPU: A Context-Bounded Model Checking Tool to Verify CUDA Programs
- Bounded Model Checking of C++ Programs based on the Qt Cross-Platform Framework
- SMT-Based Bounded Model Checking of C++ Programs

**Full List of Publications**

**Felipe R. Monteiro is currently an SDE Intern in the Automated Reasoning Group at Amazon Web Services (AWS) and is pursuing a M.Sc. degree in Computer Science at the Federal University of Amazonas (UFAM). He earned his bachelor’s degree in Computer Engineering from UFAM and he was awarded the Science without Borders scholarship, which has sponsored his studies in the Computer Science course at the Goldsmiths University of London, in 2013-2014. He has worked on 7 research and development (R&D) projects and his main experiences are in formal verification, model checking, and software engineering. His most recent work implements bounded model checking based on satisfiability modulo theories to handle formal verification of C++ programs. [Full CV]
**

**Recent Papers**

- ESBMC v6.0: Verifying C Programs using k-Induction and Invariant Inference (Competition Contribution). In TACAS, 2019.
- Towards Counterexample-guided
*k*-Induction for Fast Bug Detection. In FSE, 2018. - ESBMC 5.0: An Industrial-Strength C Model Checker. In ASE, 2018.
- Bounded Model Checking of C++ Programs based on the Qt Cross-Platform Framework: Journal-First Abstract. In ASE, 2018.

1. **Monteiro, F. R.**, Alves, E. H., Silva, I., Ismail, H. I., Cordeiro, L. C., de Lima Filho, E. B. **ESBMC-GPU: A Context-Bounded Model Checking Tool to Verify CUDA Programs.**. In Science of Computer Programming, v.152, pp. 63-69, Elsevier, 2018. DOI

2. **Monteiro, F. R.**, Januario, F. A., Cordeiro, L. C., Lima Filho, E. B. **BMCLua: A Translator for Model Checking Lua Programs**. In Software Engineering Notes, v.42(3), pp. 1-11, ACM, 2017. DOI

3. **Monteiro, F. R.**, Garcia, M. A. P., Cordeiro, L. C., Lima Filho, E. B. **Bounded Model Checking of C++ Programs based on the Qt Cross-Platform Framework**. In Software Testing, Verification and Reliability, v.27(3), pp. 1-24, 2017. The final is available at John Wiley via DOI. [Demo].

4. Pereira, P. , Albuquerque, H., Silva, I., Marques, H., **Monteiro, F. R.**, Ferreira, R. S., Cordeiro, L. C. **SMT-Based Context-Bounded Model Checking for CUDA Programs**. In Concurrency and Computation: Practice and Experience, 2016. The final publication is available at John Wiley via DOI.

5. Gadelha, M. R., **Monteiro, F. R. **, Cordeiro, L. C., Nicole, D. A. ** ESBMC v6.0: Verifying C Programs using k-Induction and Invariant Inference (Competition Contribution)**. In 25

6. Gadelha, M. R., **Monteiro, F. R. **, Cordeiro, L. C., Nicole, D. A. **Towards Counterexample-guided k-Induction for Fast Bug Detection**. In 25

7. Gadelha, M. R., **Monteiro, F. R.**, Morse, J., Cordeiro, L., Fischer, B., Nicole, D. ** ESBMC 5.0: An Industrial-Strength C Model Checker**. In 33^{rd} IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 888-891, 2018. DOI [DEMO]

8. **Monteiro, F. R.**, Garcia, M. A. P., Cordeiro, L. C., Lima Filho, E. B. **Bounded Model Checking of C++ Programs Based on the Qt Cross-Platform Framework (Journal-First Abstract)**. In 33^{rd} IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 954, 2018. DOI [Demo] and [Website].

9. Garcia, M. A. P., **Monteiro, F. R.**, Cordeiro, L. C., Lima Filho, E. B. ** ESBMC ^{QtOM}: A Bounded Model Checking Tool to Verify Qt Applications**. In 23

10. **Monteiro, F. R.**, Pereira, P. A., Cordeiro, L. C., Costa Filho, C. F. F., Costa, M. G. F. **Complementary Training Programme for Electrical and Computer Engineering Students Through an Industrial-Academic Collaboration**. In 46^{th} Annual Frontiers in Education Conference (FIE), pp. 1-9, 2016. [Presentation]

11. **Monteiro, F. R. ****Bounded model checking of state-space digital systems: the impact of finite word-length effects on the implementation of fixed-point digital controllers based on state-space modeling**. In 24^{th} ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), pp. 1151-1153, 2016. [Presentation]

12. **Monteiro, F. R.**, Cordeiro, L. C., Lima Filho, E. B. ** Bounded Model Checking of C++ Programs Based on the Qt Framework**. In IEEE 4^{th} Global Conference on Consumer Electronics (GCCE), pp. 179-180, 2015. [Poster]

13. **Monteiro, F. R.**, Cordeiro, L. C., Lima Filho, E. B. **Verificação de Programas C++ Baseados no Framework Multiplataforma Qt**. In IV Encontro Regional de Computação e Sistemas de Informação (ENCOSIS), p. 181-190, 2015. [Presentation]

14. Ramalho, M., Lopes, M., **Monteiro, F. R.**, Marques, H., Cordeiro, L. C., Fischer, B. **SMT-Based Bounded Model Checking of C++ Programs**. In 20^{th} Intl. Conf. and Workshops on the Engineering of Computer-Based Systems (ECBS), pp. 147-156, IEEE, 2013. [Presentation]

15. **Monteiro, F. R.**, COSTA, E. A. B., Castro, T. H. C. **WorldTour: Software para Suporte no Ensino de Crianças Autistas**. In 23^{rd} Brazilian Symposium on Computers in Education (SBIE), SBC, 2012.

16. **Monteiro, F. R.**, Castro, T. H. C. **WorldTour: Towards an Adaptive Software to Support Children with Autism in Tour Planning**. In IEEE 36^{th} Annual Computer Software and Applications Conference (COMPSAC), pp. 368-368, IEEE, 2012.