I, David L. Rager, am a Computer Science Ph.D. graduate from the University of Texas at Austin who defended his dissertation on August 20, 2012 and graduated in December 2012. My primary interests are security, parallel and performance computing, hardware verification, automated theorem proving, automated trading, and teaching. I currently work in the hardware verification group at Oracle.

Publications (incl. Dissertation)

Some of the work here is considered a work in progress, but much of it has reached a publishable form. See the publications index for a list of such publications. 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 had this opportunity.

Computer Architecture (CS 352) Fall 2009 TA Homepage
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


Parallel SMP Computing

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 parallel execution. 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.

Parallel Computing Efforts


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.



I like Java, and I've been fortunate enough to work with some real Java experts at Google over the last few 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.

root java source directory

User Interfaces

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.

Patches and How-to's


Most of my work involves ACL2. This section captures the topics that aren't includable in other, more broad, research areas.

ACL2 Help

Conference Organization

I was the local arrangements chair for FMCAD 2011.

Random Non-publishable "Contributions"

Figuring out Which Tag was Thrown in Lisp

Nathan Wetzler and I wrote this small thing.

Quick CCL Hashtable Examples

Warning: of little use to anyone but me. I just needed a place to stick it. Examples

Finding Global Variables in Lisp

I wrote a ruby script to find global variables in Lisp. Just from looking at it, you'll notice that it's not complete, but it's good enough for me.

Some Ideas

Do these make sense?

Other David Rager's

Alas, I'm not the only one with a cool name around:

Valid XHTML 1.1