A Tim in its natural environment.
I received my B.S. from the Computer Science department at Stanford University in 2008.
My honors thesis was supervised by David Dill.
I received my PhD from the Computer Science department at New York University in 2014.
My PhD was supervised by Clark Barrett.
I am currently a post-doctoral researcher in Verimag (UJF) working with David Monniaux.
- New email: email@example.com
- Old email:tim a firstname.lastname@example.org
(Concatenate the bolded text.)
Satisfiability modulo theories (SMT), decision procedures, software and hardware verification, saftey critical systems, automated deduction and applied logic, program analysis, and linear and mixed integer programming
Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic
Finding minimum type error sources
with Zvonimir Pavlinovic and Thomas Wies.
In Proceedings of OOPSLA, 2014. (Best Paper Award.)
[ DOI |
Leveraging Linear and Mixed Integer Programming for SMT
with Clark Barrett and Cesare Tinelli.
In Proceedings of FMCAD, 2014.
[ DOI |
Simplex with sum of infeasibilities for SMT
with Clark Barrett and Bruno Dutertre.
In Proceedings of FMCAD, 2013.
[ slides |
Exploring and categorizing error spaces using BMC and SMT
with Clark Barrett.
In Proceedings of SMT Workshop, 2011.
[ bib |
with Clark Barrett, Christopher Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Andrew Reynolds, and Cesare Tinelli
In Proceedings of CAV, 2011.
[ bib |
CVC4 and CVC3, SMT solvers
transmit: An alpha version of the transmit prototyping language. Use at own risk.
- Tiny TCAS,
finding collisions using techniques from SMT in a scaled down version of the Traffic Alert and Collision Avoidance system.
Project is in Collaboration with
MIT Lincoln Labs.