Talented and self-driven software engineer with 13+ years of work experience, I have solid problem-solving and critical-thinking skills due to my formal training in scientific research. My background in mathematics and theoretical computer science has been critical to the success of the products and innovations I consistently deliver.
Google, UK | Senior Software Engineer of Avera AI
Dec 2019 – Present
Designed and led a team of engineers to implement a cloud-based financial services product to efficiently calculate pricing and risk factors. Devised algorithms to statically analyse and transform TensorFlow code. Filed two patent applications for this work.
Google, UK | Senior Software Engineer of Chrome on Android
Aug 2014 – Dec 2019
Worked on making Chrome’s performance testing infrastructure more stable and robust. Led efforts to automatically distil hundreds of thousands of lab-gathered metrics into actionable insights for decision-makers. My work prevented significant regressions reaching billions of Chrome and WebView users on Android. And it still does.
As a 20% project, I implemented numerical optimisation algorithms in TensorFlow, halving the runtime of some production pipelines.
University College London | Computer Science Lecturer
Aug 2012 – May 2015
Designed and implemented Asterix, a theorem prover for assertions about memory allocation in computer programs, still regarded as the most efficient in its category by the research community. Taught lectures on logic and computer science theory. Awarded an EPSRC grant (£98k) to fund my research programme.
Queen Mary, University of London | Computer Science Lecturer
Jan 2012 – Aug 2012
Taught a master’s lecture on intelligent agents and multi-agent systems.
Technische Universität München | Visiting Researcher
Jan 2010 – Dec 2011
Developed an algorithm for automatically proving theorems in separation logic; this would later become the basis for Asterix.
Max Planck Institute for Software Systems | Postdoctoral Researcher
Feb 2008 – Jan 2010
Carried out research on logic programming for distributed systems. As a side project, researched the spread of content (music, news, video) through blog networks and won a best paper award for this work.
The University of Manchester | PhD in Computer Science
2004 – 2007
Conducted research into real-world applications of automated theorem proving. Funded with a scholarship (~£75k) awarded by the Mexican Council of Science and Technology.
Universidad de las Américas Puebla | Master in Computer Science
2003 – 2005
Ranked 1st in class, awarded magna cum laude. Mathematically proved the equivalence between several non-classical logic formalisms with applications to logic programming.
Universidad de las Américas Puebla | BSc in Mathematics
1999 – 2003
Ranked 1st in class, awarded magna cum laude. Began research into non-classical logic formalisms for common sense reasoning.
- Honourable Mention at the World Finals of the International Collegiate Programming Contest (ICPC), 2004.
- Third Place at the World Finals' Java Challenge of the International Collegiate Programming Contest (ICPC), 2004.
- Honourable Mention at the World Finals of the International Collegiate Programming Contest (ICPC), 2003.
- 1st Place at the National Competition of the Mexican Mathematics Olympiad, 1998.
- JA Navarro and A Rybalchenko. Separation logic + Superposition calculus = Heap theorem prover. In: Proceedings of the conference on Programming Language Design and Implementation (PLDI), 2011. ACM.
- M Cha, JA Navarro, and H Haddadi. Flash floods and ripples: The spread of media content through the blogosphere. In: Proceedings of the Annual Conference on Weblogs and Social Media (ICWSM), 2009. Winner of best paper award.
- M Osorio, JA Navarro, JR Arrazola, and V Borja. Logics with common weak completions. Journal of Logic and Computation, 16(6):867–890, 2006. Oxford University Press.
- Science communication
- Scientific skepticism
- Social justice