I am a Computer Science Ph.D. student at the University of Texas at Austin. My primary interests are security, parallel computing, and hardware design and verification. The verification unit at UT is outstanding and the security department is really starting to develop, so I am quite fortunate to be here.
Some of the work here is considered a work in progress, although most of the work worth publishing will be published by the end of 2009. Feedback is welcome.
I am and have been a Teaching Assistant for many classes. Not only does this grant me an opportunity to enrich the lives of those who will follow me, but it enables me to practice communication. Given it's easy to bury my head in a solitary world while working on a Ph.D., I am fortunate to have this opportunity. Also, I've never had the experience of working as a waiter or holding another blue-collar job. Although being a TA is still white-collar, there's not much thrill to grading papers (but helping students can be rewarding), and so the job builds my character.
Logic, Sets, and Functions (CS 313K) Spring 2009 TA Homepage
An Integrated Approach to Verification and
Validation of Software Systems (CS 378) Fall 2008 TA Homepage
Computer Architecture (CS 352) Spring 2008 TA Homepage
Programming Languages (CS 345) Spring 2007 TA Homepage
Computer Architecture (CS 352) Fall 2006 TA Homepage
Multi-core processors are the latest rage. As such, we'd like to use the hardware computing resources available to us. In a functional language like ACL2, if the user had the right efficient constructs, it would be completely safe (although not neccessarily live) to introduce parallelism. The parallelism library described below experiences a speedup of 7x when run on an 8-core SMP machine on toy problems such as the doubly recursive Fibonacci function. Unfortunately, performance degrades significantly whenever a good granularity form cannot be found or when the algorithm is garbage generation intense. Since the LISPs we use have serial garbage collectors, this garbage collection time is a major drawback. For more information, please see the page below on parallelism.
I like Java, and I've been fortunate enough to work with some real Java experts at Google over the last couple summers. As such, my interest in it has grown, and I've got some random projects related to it. The only thing I'm placing here is my creation of a RangedMap class. This class uses a Differable interface (another creation) to estimate the differences between Objects, and then provides a Value for the Key closest to the Key provided in the lookup. I found them useful so I'm sharing them in the below directories.
I've been interested in security since the early 2000's. The first paper on a verification effort for key-establishment protocol JFKr was published in the ACL2 2009 workshop. Also included below are a survey of the wireless protocols in existence in the year 2004. This survey also provides guidelines for evaluation of future wireless protocols. In 2003, a UT student allegedly obtained some social security numbers via "hacking." You will also find a report giving some details and explanations of the related laws. This report was written for a class in my earlier years, so please forgive me if it contains something incorrect.
Wouldn't it be great if an ACL2 user could more quickly find what changed from one form's printing to the next? Doing so would allow them to find typos in their code more quickly, reducing their overall proof time. What if ACL2 hid parts of terms heuristically irrelevant to the user? That too would save the user some time. Below are the patches and supporting documents that an ACL2 user can use to enable term hiding and highlighting for ACL2 2.9.1.
Alas, I'm not the only one with a cool name around:
Do these make sense?