Selected Papers
Full List of Publications
Felipe R. Monteiro is an Applied Scientist with the Automated Reasoning Group at Amazon. His main experiences are in static analysis, model checking, and software verification and his most recent work combines proof decomposition with model checking to verify complex software systems. [Full CV]
Recent Papers
Apr 09. I gave a talk at the 4th Rust Verification Workshop
2023Dec 08. I gave a talk at the 26th Brazilian Symposium on Formal Methods
Aug 31. Check out our new blog post on the Kani Rust Verifier Blog!
Monteiro, F. R., Gadelha, M. R., Menezes, R., Cordeiro, L. C. Summary of Model Checking C++ Programs. In 15th IEEE International Conference on Software Testing, Verification and Validation (ICST), 2022.
Gadelha, M. R., Menezes, R., Monteiro, F. R., Cordeiro, L. C., and Nicole, D. A. ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory (Competition Contribution). In 23rd International Conference on Fundamental Approaches to Software Engineering (FASE), 2020.
Chong, N., Cook, B., Kallas, K., Khazem, K., Monteiro, F. R., Schwartz-Narbonne, D., Tasiran, S., Tautschnig, M., Tuttle, M. R. Code-Level Model Checking in the Software Development Workflow. In 42nd International Conference on Software Engineering (ICSE), 2020.
Monteiro, F. R. , Gadelha, M. R., and Cordeiro, L. C. Boost the Impact of Continuous Formal Verification in Industry. In 10th Workshop on Tools for Automatic Program Analysis (TAPAS), pp. 41-47, 2019.
Gadelha, M. R., Monteiro, F. R. , Cordeiro, L. C., and Nicole, D. A. ESBMC v6.0: Verifying C Programs using k-Induction and Invariant Inference (Competition Contribution). In 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 11429, pp. 1-5, 2019.
Gadelha, M. R., Monteiro, F. R. , Cordeiro, L. C., Nicole, D. A. Towards Counterexample-guided k-Induction for Fast Bug Detection. In 25th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (ESEC/FSE), 2018.
Gadelha, M. R., Monteiro, F. R., Morse, J., Cordeiro, L., Fischer, B., Nicole, D. ESBMC 5.0: An Industrial-Strength C Model Checker. In 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 888-891, 2018. DOI [DEMO]
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 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 954, 2018. DOI [Demo] and [Website].
Garcia, M. A. P., Monteiro, F. R., Cordeiro, L. C., Lima Filho, E. B. ESBMCQtOM: A Bounded Model Checking Tool to Verify Qt Applications. In 23rd International SPIN symposium on Model Checking of Software (SPIN), LNCS 9641, pp. 97-103, 2016. [Presentation] and [Demo].
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 46th Annual Frontiers in Education Conference (FIE), pp. 1-9, 2016. [Presentation]
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 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE), pp. 1151-1153, 2016. [Presentation]
Monteiro, F. R., Cordeiro, L. C., Lima Filho, E. B. Bounded Model Checking of C++ Programs Based on the Qt Framework. In IEEE 4th Global Conference on Consumer Electronics (GCCE), pp. 179-180, 2015. [Poster]
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]
Ramalho, M., Lopes, M., Monteiro, F. R., Marques, H., Cordeiro, L. C., Fischer, B. SMT-Based Bounded Model Checking of C++ Programs. In 20th Intl. Conf. and Workshops on the Engineering of Computer-Based Systems (ECBS), pp. 147-156, IEEE, 2013. [Presentation]
Monteiro, F. R., COSTA, E. A. B., Castro, T. H. C. WorldTour: Software para Suporte no Ensino de Crianças Autistas. In 23rd Brazilian Symposium on Computers in Education (SBIE), SBC, 2012.
Monteiro, F. R., Castro, T. H. C. WorldTour: Towards an Adaptive Software to Support Children with Autism in Tour Planning. In IEEE 36th Annual Computer Software and Applications Conference (COMPSAC), pp. 368-368, IEEE, 2012.
Monteiro, F. R., Gadelha, M. R., and Cordeiro, L. C. Model Checking C++ Programs. In Softw Test Verif Reliab, v.32, pp. e1793, 2022.
Chong, N., Cook, B., Kallas, K., Khazem, K., Monteiro, F. R., Schwartz-Narbonne, D., Tasiran, S., Tautschnig, M., Tuttle, M. R. Code-Level Model Checking in the Software Development Workflow at Amazon Web Services. In Softw: Pract Exper, v.51, pp. 772–797, 2021.
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
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
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].
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.
Monteiro, F. R. Formal Verification to Ensuring the Memory Safety of C++ Programs. M.Sc. Thesis, Federal University of Amazonas, 2020. [Presentation]
2018
External Reviewer of the VIII Brazilian Symposium on Computing Systems Engineering (SBESC), 2018.
Program committee / Jury member of the 7th Intl. Competition on Software Verification (SV-COMP), 2018.
2019
Artifact evaluation committee member of the 13th Intl. Conference on Tests and Proofs (TAP), 2019.
Reviewer of the journal IEEE Access, 2019.
2020
Program committee / Jury member of the 9th Intl. Competition on Software Verification (SV-COMP), 2020.
2021
Program committee / Jury member of the 10th Intl. Competition on Software Verification (SV-COMP), 2021.
Artifact evaluation committee member of the Object Oriented Programming Languages, Systems and Applications (OOPSLA), 2021.
2022
Artifact evaluation committee member of the 34th Intl. Conference on Computer Aided Verification (CAV), 2022.
2023
Program committee member of the 24th Intl. Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2023.
Artifact evaluation committee member of the 24th Intl. Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2023.
Artifact evaluation committee member of the 29th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2023.
Artifact evaluation committee member of the 32nd ACM SIGSOFT Intl. Symposium on Software Testing and Analysis (ISSTA), 2023.
2024
Artifact evaluation committee member of the 30th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2024.
