My name is Federico Mora Rocha. I am currently an applied scientist at Amazon Web Services. Starting fall 2026, I will be an assistant professor of computer science at the University of Waterloo and a faculty affiliate at the Vector Institute.
I study automated reasoning, programming language theory, and neuro-symbolic artificial intelligence. For more information about my work, see my curriculum vitae.
| 04/2026 | Gave an Invited Talk at VerifAI-2 |
| 04/2026 | Won the David J. Sakrison Memorial Prize |
| 11/2025 | Gave an Expo Demonstration at NeurIPS 2025 |
| 08/2025 | Graduated from the University of California, Berkeley |
| 07/2025 | Accepted Tenure-Track Faculty Position at the University of Waterloo |
| 07/2024 | Won the QF_Datatypes division of SMT-COMP 2024 |
| 05/2024 | Amar Shah Won Silver at the ACM SRC Grand Finals |
| 04/2024 | Won Outstanding Graduate Student Peer Mentor Award |
| 04/2024 | Won Demetri Angelakos Memorial Achievement Award |
| 10/2023 | Haley Lepe won National Diversity in STEM Conference Presentation Award |
| 06/2023 | Amar Shah won PLDI Undergraduate Student Research Competition |
| 05/2023 | Won Outstanding TA Award |
| 02/2023 | Passed Qualifying Exam |
| 05/2022 | Won Outstanding GSI Award |
| 03/2022 | African American Museum and Library Recommends my Map |
| 07/2021 | Won Qualcomm Innovation Fellowship |
| 01/2020 | Murad Akhundov won POPL Undergraduate Student Research Competition |
| ICRA '26 | Learning Affordances at Inference-Time for Vision-Language-Action Models |
| Thesis '25 | Scalable and Usable Domain-Specific Automated Reasoning |
| AAAI '25 | Online Prompt Selection for Program Synthesis |
| NeurIPS '24 | Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages |
| AAAI '24 | An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes |
| TCS '23 | Towards more efficient methods for solving regular-expression heavy string constraints |
| SYNT '23 | Genetic Algorithms for Searching a Matrix of Metagrammars for Synthesis |
| OOPSLA '23 | Message Chains for Distributed System Verification |
| CAV '22 | UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis |
| WORDS '21 | String Theories involving Regular Membership Predicates: From Practice to Theory and Back |
| SAT '21 | MedleySolver: Online SMT Algorithm Selection |
| FM '21 | Z3str4: A Multi-armed String Solver |
| FM '21 | BanditFuzz: Fuzzing SMT Solvers with Multi-Agent Reinforcement Learning |
| CAV '21 | An SMT Solver for Regular Expressions and Linear Arithmetic over String Length |
| ATVA '21 | Verification by Gambling on Program Slices |
| VSTTE '20 | BanditFuzz: A Reinforcement-Learning Based Performance Fuzzer for SMT Solvers |
| SYNT '20 | Synthesis in UCLID5 |
| ASE '20 | Scaling Client-Specific Equivalence Checking via Impact Boundary Search |
| CAV '18 | StringFuzz: A Fuzzer for String Solvers |
| ASE '18 | Client-Specific Equivalence Checking |
I am looking for graduate students to join my group! If you are interested, please list my name as a potential advisor in your application.
| 2026 | David J. Sakrison Memorial Prize |
| 2025 | NeurIPS Top Reviewer |
| 2024 | QF_Datatypes division of SMT-COMP |
| 2024 | Outstanding Graduate Student Peer Mentor Award |
| 2024 | Demetri Angelakos Memorial Achievement Award |
| 2023 | Outstanding Teaching Assistant Award |
| 2022 | Outstanding Graduate Student Instructor Award |
| 2021 | Qualcomm Innovation Fellowship |
| 2021 | Chair's Graduate Award |
| 2019 | Department Fellowship |
| 2018 | C. C. Gotlieb (Kelly) Graduate Fellowship |
| 2017 | Alfred B. Lehman Graduate Scholarship |