Dr. R. Dustin Wehr
Work Experience
Amazon Web Services (Aurora Serverless team)
March 2021 – May 2022
Software Development Engineer
Aurora Serverless provides managed replicated MySQL and PostgreSQL services that can vertically autoscale, restart, and patch, all without dropping connections. I worked on the Control Plane team.
Highlights
- Enhancement, maintenance, and operation of a system managing hundreds of thousands of MySQL and PostgreSQL databases. It is a distributed system with five major service node types, in addition to many AWS services.
- Contributed to design of the next generation "heat management" optimization for Aurora Serverless V2, which is the system that decides where to place Aurora instances on the multi tenant oversubscribed hosts, and what live migrations to do in order to alleviate overloaded hosts. It is a combination of ML for predicting instance resource needs (CPU, memory, network IO) and stochastic/robust mixed integer programming for decisions (with work on a RL agent on the horizon).
- CI/CD, Unit and integration testing, design docs, code reviews
- Java for main application. React, Python, shell scripting for dev and ops tools. Ruby for infrastructure-as-code.
- Regular use of many AWS technologies including Lambda, S3, DynamoDB, CloudWatch/CloudFormation/CodeDeploy, various RDS services, SWF, Step Functions.
DaGoods Inc.
August 2022 – March 2023
Full stack developer / Co-Founder
Sourcing and selling on online marketplaces (Amazon, Ebay, etc).
Highlights
- Writing custom software, including:
- A barcode-driven inventory, stocking, and picking app, tailored for the business (stock in many locations, scarce convenient locations, large number of SKUs).
- Conflict-free, offline-friendly multi-device support, using nothing but an end-user cloud storage provider (Dropbox, Google Drive, etc).
- An OCR tool for integrating an integration-unfriendly selling platform into our shipping provider.
- A phone tool that helps with product research specific to business's niche.
- A barcode-driven inventory, stocking, and picking app, tailored for the business (stock in many locations, scarce convenient locations, large number of SKUs).
- Product sourcing and selling strategy. More than 200% sales growth during my tenure.
- Most of the legal and bookkeeping work.
- Customer service for the Amazon marketplaces (we had 100% positive feedback) and the harder Ebay cases.
INNOV-8
February 2020 – May 2020
Data Science and AI Engineer
A legal tech startup. There wasn't any AI to do, as my title suggested, but I did fill an assortment of tech needs, getting the company through its first four months. Several e-discovery data collections and basic processing/analyses, including a large one (250TB+) spread over a messy network of a bankrupt company. Helped build the company's knowledge management infrastructure. Helped the team cope with Office 365. Greatly improved the load time of their marketing-team-created website, without breaking the conventions that make it generable from their content management system.
Research Engineer and Formal Logic/Languages Specialist
R&D lead for the development of open source software and specifications for writing legally binding contracts in formal languages.
Highlights
- Critical role in securing $15 million government/industry/academic collaboration grant for the Centre for Computational Law in Singapore, which opened in mid 2020. Lest there be any uncertainty, by "critical" I mean that it would not have happened without me!
- Designed and implemented the company’s planned-to-be open source DSL for computational legal contracts, with support for testing, model checking, formal verification, scenario exploration, visualization, and some preliminary support for natural language generation and smart contract deployment.
- Python, Scala, Z3 and other SMTLib2 solvers, Timed Automata solvers, Coq
Software Engineering Consultant
Supervised a modernization of EXAKT, a highly advanced Condition Based Maintenance policy optimizer that was trapped in a legacy Windows C++ codebase. Also worked on integrating it with Living Reliability's Mesh software, a web portal for maintenance operations.
Software Engineering Consultant
Data processing and analysis for a project at the BP Whiting Refinery. Used my project Structure Together (it made some money!) and Python.
Centre for Maintenance Optimization and Reliability Engineering (University of Toronto, MIE Department)
September 2016 – December 2016
Postdoc
Continuation of work on EXAKT (see Optimal Maintenance Decisions job above), but additionally collaborating with the principal statistician and academic engineers responsible for its methods.
Software Developer / Machine Learning Consultant
LSTM recurrent neural net project for an art exhibit. I generated a fake group chat stream from years of the client art collective's WhatsApp group chat conversations. Used PyTorch.
Software Developer
Built novel TV and movie recommendation sites. Hired with raise after internship, but only for a few months as I had to return to graduate studies.
Highlights
- Data Science, Scala, HTML/Javascript, Python, PostgreSQL
- https://www.pcworld.com/article/2044340/televisor-is-your-personalized-tv-critic-for-streaming-shows.html
University of Toronto
January 2015 – April 2015
Lecturer
Introduction to the Theory of Computation (CSC236), a second-year proof-based course. Both this course and the previous year's course (below) involved managing teams of teaching assistants, and working closely with other lecturers, both in-person and remote.
University of Toronto
January 2014 – April 2014
Lecturer
Introduction to Computer Science (CSC148). We used Python 3.
Self-employed
March 2015 – August 2017
Tutor for various undergraduate CS courses
Easy money.
Web Developer
Fixed various problems / made various improvements on a BigCommerce e-commerce site. This was for a relative of a friend.
University of Toronto
September 2008 – January 2015
Some Graduate Studies...
Highlights
- See elsewhere in this resume for publications
- Presented my proof of a conjecture made by Anna Gál, Michal Koucký, and Pierre McKenzie in their 2008 journal paper “Incremental Branching Programs” at the BIRS workshop “Computational Complexity”, August 1-6, 2010. Writeup for the proof: https://arxiv.org/abs/1101.2705.
- Solved an open problem in the summer preceding graduate school that had four brilliant complexity theorists stumped for a while (lower bound for fractional pebbling trees).
- Did a well-received project for Professor Geoffrey Hinton's Machine Learning graduate course, where my partner and I made some modest, but definite and transferable, improvements on the groundbreaking recommendation system work of Ruslan Salakhutdinov, Andriy Mnih, and Geoffrey Hinton that kicked off the Deep Learning boom. Final writeup for the project: https://www.cs.toronto.edu/~wehr/ restricted_boltzmann_machines_netflix_CSC2515report.pdf
- Gave a two-hour lecture on Software Transactional Memory for the graduate course Advanced Distributed Computing. I am well informed on the theory up till that date (over five years ago).
University of Toronto
September 2008 – April 2015
Teaching Assistant
Held several teaching assistantships throughout my graduate studies, all of which I was encouraged to repeat.
Highlights
- Computability and Logic, graduate/undergraduate, multiple semesters
- Computational Complexity and Computability, multiple semesters
- Introduction to Computational Complexity, graduate
- Principles of Programming Languages
- Introduction to Theory of Computing, multiple semesters
- Help Centre for all CS courses, multiple semesters
McGill, Software Evolution and Verification Lab
May 2007 – August 2007
Student Researcher
Work on a prototype programming language, developed by Professor Brigitte Pientka, for writing provably-correct programs, especially complex syntax-manipulating programs such as compilers. Programming in SML and the logic-programming language Twelf.
McGill, CS Department
June 2006 – December 2007
Teaching Assistant
Held several teaching assistantships throughout my undergraduate studies. This is fairly common since the surge in CS enrollment, but was quite rare back then.
Highlights
- Logic and Computability, multiple semesters
- Principles of Statistics I
McGill, Centre for Intelligent Machines
May 2006 – August 2006
Student Researcher
Recommendation systems research, supervised by Professor Greg Dudek. Programming mostly in MatLab.
U.S. Airforce Research Lab at Wright Patterson Air Force Base
June 2005 – August 2005
Student Research Assistant
Highlights
- Worked on techniques for data mining of (primitive, by today’s standards!) social networks that depict e.g. communication relationships between possible terrorists.
- Software for processing and viewing/analyzing data from experiments that involved groups of military personnel interacting in a virtual space.
- Python, Java
U.S. Airforce Research Lab at Wright Patterson Air Force Base
May 2004 – September 2004
Student Research Assistant
In the Electrical Technology and Plasma Physics Branch.
Highlights
- Performed experiments related to improving techniques for growing (in a plasma reactor) thin diamond films by boron doping.
- Wrote some code for Dr. Alan Garscadden for losslessly converting image files created by some old lab equipment to a standard format.
Skills
Highlighted Knowledge
OOP
AWS
Distributed Computing
Linux
Web Applications
React
HTML/CSS
Automated Theorem Proving
Formal Specification and Verification
Algorithms
Language Design
Bayesian Statistics
Neural Networks
PLs (fluent)
Java
Python
Scala
TypeScript
PLs (familiar or rusty)
C
Kotlin
Ruby
TLA+/PlusCal
SML
C++
Mathematica
MatLab
Publications
Packing Two Circles with One Cut by a Chord
28 March 2021
Computer-assisted resolution of a 55-year old open problem in elementary recreational geometry: What is the smallest square that can fit two unit circles, one of which is cut in two by a chord? NOTE abstract and introduction are silly, but the proof is legit.
Errors in Bostrom/Kulczycki Simulation Arguments
12 February 2017
Demonstrated that Bostrom et. al.'s Simulation Arguments, including the "patched" ones, have errors that result in inconsistent and greatly misleading glosses (implying, for example, that 1 is "vastly greater than" 989,901). Gave corrected, rigorous, necessarily-less-impressive versions of the arguments.
PhD Thesis: Rigorous Deductive Argumentation for Socially Relevant Issues
University of Toronto Press
30 January 2015
Laid out a program for how formal logic can be used, in an interactive environment and in combination with natural language, to improve deliberation and debate on questions that formal logic and mathematics are usually thought unsuitable for: those involving significant vagueness, subjectiveness, and uncertainty.
Challenges and Examples of Rigorous Deductive Reasoning About Socially-Relevant Issues
Trends in Logic XIV
01 May 2014
Roughly a small fraction of PhD Thesis
Pebbles and Branching Programs for the Tree Evaluation Problem
ACM Transactions on Computation Theory
01 May 2010
Stephen A. Cook, Pierre McKenzie, Dustin Wehr, Mark Braverman, Rahul Santhanam
Branching Programs for Tree Evaluation
Mathematical Foundations of Computer Science
01 January 2009
Mark Braverman, Stephen A. Cook, Pierre McKenzie, Rahul Santhanam, Dustin Wehr
Fractional Pebbling and Thrifty Branching Programs
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
15 December 2008
Mark Braverman, Stephen A. Cook, Pierre McKenzie, Rahul Santhanam, Dustin Wehr
Projects
- Where's My Stuff? (backburner): An (optionally) voice-controlled, offline-first, web-based collaborative (multi-user) inventory, built at first for my own use for organizing my things and trading/selling/gifting found things. The currently deployed prototype uses the prohibitively-expensive (at scale) Firebase for backend. Will merge this with the DaGoods Inventory app in the future, which uses a free user-friendly self-owned backend. Prototype written in Typescript, HTML.
- Structure Together (backburner): Still the most advanced realtime-collaborative Structure Editor, as far as I know. I made it for Logic for Progress, but I have not given it the polishing and publicity that it deserves. This includes my best front-end work, so if that interests you let me know, and I'll put some time into porting it from the discontinued Google Realtime API to Firebase. TypeScript, HTML, React, Google Closure Compiler, Webpack.
- Mingaling (completed, discontinued): First-of-its kind browser extension for practicing vocabulary of a second language while reading text in one's primary language, by substitution of selected words. There were a few thousand users at some point, despite no attempt made to advertise it. Mozilla appears to have dumped the old use statistics, but I can still see the review distribution (all 5 stars, 19 reviews). Review from a language learning site: pdf archive or ancient link: https://www.ghacks.net/2011/03/27/ming-a-ling-language-learning-add-on-for-firefox. A successful current commercial effort: https://chrome.google.com/webstore/detail/toucan-language-learning/lokjgaehpcnlmkebpmjiofccpklbmoci?hl=en. JavaScript, HTML, AJAX.
Education
-
2008 2015
University of Toronto
PhD/MSc
Computer Science
Courses- Advanced Distributed Computing
- Machine Learning
- Algorithm Design, Analysis and Theory
- Theory of Distributed Computing
- Fundamentals of Cryptography
- Algorithms for Solving Propositional Theories
- Complexity Theory
- Topics in Knowledge Representation and Reasoning
-
2004 2008
McGill University
BSc
Computer Science
Courses- Probabilistic Reasoning and Artificial Intelligence
- Formal Verification
- Probabilistic Analysis of Algorithms
- Automated Reasoning
- Language-Based Security
- Algorithm Design Techniques
- Theoretical Programming Languages
Volunteer
Web Developer
Made various improvements to the Charity Intelligence website, including a major feature to inform donors about higher performing charities that are similar to the one they are reading about.
CEO/Cofounder
Logic for Progress is a registered non-profit that aims to advance the quality of deliberation on contentious social issues, in part by leveraging the exceptionally high standards of formal deductive logic. The approach helps to "cut through the noise" to find the fundamental sources of disagreement, even for some highly contentious issues, while also helping to avoid the pitfalls of reductionist mathematical modeling typical of e.g. economics and game theory, and the manipulability of popular statistical methods. Continuation and implementation of my PhD work.
Awards
-
January 2017
Charity Intelligence
Volunteer of the Year
-
September 2008
NSERC
Postgraduate Scholarship M
Sep 2008 - Sep 2010 (renewed once)
-
September 2008
University of Toronto CS Department
Helen Sawyer Hogg Award
Graduate entrance scholarship
-
May 2007
McGill Faculty of Science
Science Undergraduate Research Award
Summer 2007
-
May 2006
NSERC / McGill
Undergraduate Student Research Award
Summer 2006
-
September 2004
McGill
Hugh Brock Scholarship
Undergraduate entrance scholarship, 2004 - 2008