Headshot

My name is Federico Mora Rocha. I am a Ph.D. student in computer science at the University of California, Berkeley, where I am advised by Sanjit A. Seshia. Before Berkeley, I completed an M.Sc. in computer science at the University of Toronto, where I was advised by Marsha Chechik. Before Toronto, I completed a B.Sc. in computer science and mathematics at Mount Allison University.

My primary areas of expertise are automated reasoning, formal methods, and programming language theory.

I am on the job market this year! Here is my CV (pdf), research statement (pdf, html), teaching statement (pdf, html), Google Scholar profile (html), and DBLP profile (html). You can reach me at fmora@cs.berkeley.edu.

Recent News (see all)

07/2024
We won the QF_Datatypes division of SMT-COMP 2024!
05/2024
Amar Shah, my mentee, came second at the 2024 ACM SRC Grand Finals!
04/2024
I won UC Berkeley's Outstanding Graduate Student Peer Mentor Award!
04/2024
I won the Demetri Angelakos Memorial Achievement Award!
02/2024
I presented our paper on an eager SMT solver for ADTs at AAAI '24

Selected Publications (see all)

(undergraduate mentees underlined)

Refereed Conference Papers

NeurIPS '24
NeurIPS '24
Synthetic Programming Elicitation for Text-to-Code in Very
Low-Resource Programming and Formal Languages
F. Mora, J. Wong, H. Lepe, S. Bhatia, K. Elmaaroufi,
G. Varghese, J. E. Gonzalez, E. Polgreen and S. A. Seshia
AAAI '24
An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes
A. Shah, F. Mora and S. A. Seshia
OOPSLA '23
OOPSLA '23
Message Chains for Distributed System Verification
F. Mora, A. Desai, E. Polgreen and S. A. Seshia
FM '21
Z3str4: A Multi-armed String Solver
F. Mora, M. Berzish, M. Kulczynski, D. Nowotka and V. Ganesh
SAT '21
MedleySolver: Online SMT Algorithm Selection
N. Pimpalkhare, F. Mora, E. Polgreen and S. A. Seshia
CAV '21
An SMT Solver for Regular Expressions and
Linear Arithmetic over String Length
M. Berzish, M. Kulczynski, F. Mora, F. Manea,
J. Day, D. Nowotka and V. Ganesh

Refereed Short or Tool Papers

CAV '22
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
E. Polgreen, K. Cheang, P. Gaddamadugu, A. Godbole, K. Laeufer,
S. Lin, Y. Manerkar, F. Mora and S. A. Seshia
CAV '18
StringFuzz: A Fuzzer for String Solvers
D. Blotsky, F. Mora, M. Berzish, Y. Zheng, I. Kabir and V. Ganesh