and I have funding. My research is primarily in formal verification, especially as it relates to VLSI design. What that really means is I like using mathematical logic and methods from other branches of mathematics, especially dynamical systems theory, to solve interesting problems that arise in the design of computational hardware and software. This also gives me interests in many connecting areas including parallel computation, scientific computing, software verification, security, machine learning, and robotics. You can find our more about my research here.

I'll list some of the ideas I'm currently working on and would be happy to work on, but before I scare you off,
I'll put this in context.
**My work is very interdisciplinary. I don't expect incoming students to have a background that combines
mathematical logic, formal verification, VLSI design, scientific computing, and whatever other areas we may
branch into. What I am looking for are students who are eager to learn.**
Along the way, you can take classes, and I'll teach you the areas you need for your research.
If you like solving puzzles and want to work on cutting edge research that has real impact in industry,
verification is probably a good fit for you.

Most undergraduate programs don't cover as many areas as my research; so, I often get asked: “What can I do once I've done research with you?” Plenty. This work give you a very top-to-bottom understanding of computing -- think “full-stack developer”, only more so. I have former students at Amazon, Cisco, Electronic Arts, FitBit, IBM, Google, Intel, Oracle, Synopsis, UBC, and many other top places -- where do you want to go? I view an internship at an industry research lab as a great part of any Ph.D.\ program, and my colleagues in industry are frequently asking me for more interns.

Here are some examples of areas where I am currently looking for new students:

- Analog and mixed-signal verification. Applications of linear systems theory to verifying large mixed-signal functions. Circuit modeling and optimal control techniques for circuit synthesis and analysis.
- Theorem-proving and SMT: combining fully automatic decision procedures (e.g. the SMT solvers such as Z3, download here) with interactive theorem provers (e.g. ACL2).
- Applications in software development and security, machine learning, and robotics.
- What would you like to do?

Last Modified: August 16, 2015