Talented and self-driven software engineer with 15+ 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.
Employment
Google, UK | Staff Software Engineer
Aug 2014 – Present
Capital Markets Technology: Tech lead of team in Google Cloud.
Avera AI: Led a team of engineers to implement a cloud-based financial services product for efficiently calculating pricing and risk factors. Devised algorithms to statically analyse and transform TensorFlow code. Filed two patent applications.
Chrome on Android: Made 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 from reaching billions of Chrome and WebView users on Android. And it still does.
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.
Education
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.
Notable awards
- 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.
Selected publications
- 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.
Patents
- A Saxena, VB Vega, M Rizman, P Shmakov, JA Navarro, and C Chimisov. Automatic Memory Management for Compute Graphs. US20240193421A1, filed 9 Dec 2022. Patent pending.
- A Saxena, JA Navarro, P Shmakov, C Chimisov, VB Vega, M Rizman, and M Pearce. Graph Execution Engine. US20230185622A1, filed 13 Dec 2021. Patent pending.
Interests
- Philosophy
- Ethics
- Science communication
- Scientific skepticism
- Lego
- Food
- Cooking
- Humanism
- Social justice