|
My name is Federico Mora Rocha and I’m an Applied Scientist in the Automated Reasoning Group (ARG) at Amazon Web Services (AWS). Starting Fall 2026, I will be an Assistant Professor in the Cheriton School of Computer Science at the University of Waterloo and a Faculty Affiliate at the Vector Institute. |
| 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 |
| 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 |
If you are interested in automated reasoning, programming languages, or neuro-symbolic systems, please take a look at my recent publications and consider applying to join my group!
| 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 |
