CV

Contact Information

Name Felipe R. Monteiro
Professional Title Senior Applied Scientist
Email felisous@amazon.com
Location 7 W 34th St, New York, New York NY 10001

Professional Summary

Senior Applied Scientist at the AWS Automated Reasoning Group. Research combines automated reasoning and neuro-symbolic AI to improve LLM-agent reliability, with soundness as the north star. Background in software verification of C, C++, and Rust.

Experience

  • 2026 - Present

    New York, NY

    Senior Applied Scientist
    Amazon Web Services
    Research combining automated reasoning and neuro-symbolic AI to improve LLM-agent reliability.
    • Automated Reasoning Group
  • 2021 - 2026

    New York, NY

    Applied Scientist II
    Amazon Web Services
    Research on compositional techniques and model checking. Proving memory safety and functional correctness of system-level code. Combining automated reasoning tools with LLMs to produce formally verified programs.
    • Automated Reasoning Group
  • 2020 - 2021

    New York, NY

    SDE-II
    Amazon Web Services
    Research on continuous software verification, static analysis, and model checking. Proving memory safety and functional correctness of system-level code.
    • Automated Reasoning Group
  • 2019 - 2019

    New York, NY

    SDE-I Intern
    Amazon Web Services
    Research on software verification and model checking. Development of proof harnesses for a core C99 package including cross-platform primitives, configuration, data structures, and error handling.
    • Automated Reasoning Group
  • 2018 - 2019

    Manaus, Brazil

    Software Engineer
    Eldorado Institute
    Research on battery management for Android-based smartphones. Development of an Android application to perform stress test hardware components and measure current drain.
  • 2011 - 2017

    Manaus, Brazil

    Undergraduate Research Fellow and Developer
    Electronic and Information Research Center
    Research on formal verification of digital systems (DSVerifier), model checking of C++ programs based on the Qt framework (QtOM), and model checking of CUDA-based applications (ESBMC-GPU).
    • Systems & Software Verification Laboratory
  • 2017 - 2017

    Seattle, WA

    Google Summer of Code Intern
    University of Washington
    Research on whole-program inference for the Checker Framework. Sponsored by Google.
    • Google Summer of Code 2017
  • 2015 - 2016

    Manaus, Brazil

    Undergraduate Research Fellow
    Samsung Electronics
    Mobile application development (Android). Led, architected, and participated in the design, testing, and deployment of an Android application. Participated as Scrum Master.
  • 2011 - 2013

    Manaus, Brazil

    Undergraduate Research Fellow
    Institute of Technology Development (INdT)
    Research on formal verification of C++ programs using SMT-based BMC (ESBMC++).
    • Systems & Software Verification Laboratory
  • 2011 - 2011

    Manaus, Brazil

    Undergraduate Research Fellow
    Institute of Computing
    Research on assistive technology for autistic children. Usability and semiotic engineering of human-computer interaction.
    • Laboratory of Intelligent Systems

Education

  • 2018 - 2020

    Manaus, Brazil

    M.Sc.
    Federal University of Amazonas
    Computer Science
  • 2011 - 2018

    Manaus, Brazil

    B.Eng.
    Federal University of Amazonas
    Computer Engineering
  • 2013 - 2014

    London, UK

    Exchange Program
    Goldsmiths University of London
    Computer Science

Awards

  • 2018
    Woody Bledsoe Award
    9th International Joint Conference on Automated Reasoning

  • 2016
    Silver Medal at the International ACM Student Research Competition
    Association for Computing Machines

  • 2016
    Best Mobile Application Award
    3rd Technological Innovation Summit, Samsung Electronics of Amazonia

Skills

Formal Methods (): Model Checking, Static Analysis, Software Verification, Automated Reasoning, SMT Solvers
Programming Languages (): C/C++, Rust, Python, Java
AI & Machine Learning (): Neuro-symbolic AI, LLM Agents, Program Synthesis

Languages

Portuguese : Native speaker
English : Fluent

Projects

  • 2019 - Present
    CBMC

    A Bounded Model Checker for C and C++ programs.

  • 2021 - Present
    Kani

    A model checker for Rust programs.

  • 2024 - Present
    Verify Rust Std

    Crowdsourced verification of the Rust Standard Library.

  • 2011 - Present
    ESBMC

    An industrial-strength context-bounded model checker for C/C++.

  • 2014 - Present
    DSVerifier

    A bounded model checker for digital systems verification.

  • 2017 - 2017
    Checker Framework

    Enhances Java’s type system to detect and prevent errors. Contributed to the whole-program inference module.