Programming Languages Lab
Room ECCS 1B11
University of Colorado Engineering Center
Boulder, CO 80309 USA
École Normale Supérieure
45 Rue d'Ulm
75230 Paris Cedex 05 France
I am a Ph.D. student studying automatic software verification at both the University of Colorado Boulder and at École Normale Supérieure. I am co-advised by Dr. Bor-Yuh Evan Chang, Dr. Xavier Rival, and Dr. Sriram Sankaranarayanan. I belong to the University of Colorado Programming Languages and Verification (CUPLV) group. In addition to researching verification of dynamic programming languages, I play saxophone, take pictures, and design and build electronics and software.
June 2014 - My paper Automatic Analysis of Open Objects in Dynamic Language Programs has been accepted to SAS 2014.
May 2014 - The preprint of the QUICr paper is now available.
April 2014 - My tool paper QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers has been accepted to CAV 2014.
June 2013 - My journal paper on unbounded and bounded digital filter verification has been published in STTT.
April 2013 - My paper on QUIC Graphs was accepted at ECOOP 2013
In a partnership with ioSemantics, I am working on automated program analysis of business logic software. I am investigating high performance methods of using Satisfiability Modulo Theories solvers to explore the possible state space of programs.
The Incremental Inductive Model Checker was a project of the Model Checking group at the University of Colorado at Boulder. I investigated combinational optimizations for encoding problems for SAT. I implemented the Tseitin Transform, technology mapping (Eén, Mishchenko and Sörensson). The code for this project is not yet available and may never become available.
I implemented technology mapping for CNF conversion for the IC3 model checker. This model checker placed 3rd in the HWMCC10 competition. The technology mapping used in IC3 is primitive compared to that used in IImc.
Prior to returning to school for graduate study, I worked for Agere Systems (acquired by LSI) as a digital design engineer. I developed Verilog designs for a hard disk read channel. A read channel is responsible for converting the analog electrical signals that come from a Giant Magnetoresistance (GMR) head into the digital data that a computer can interpret. It does this using a Viterbi decoder.
I worked on a variety of parts of the chip. I first developed test circuitry to help in the characterization of the analog amplifiers, filters and converters. Later I did an end-to-end design of a clock generator, modernizing RTL for verification and static timing and performing a standard cell layout using the standard tools of the time. This design involved integrating analog and digital components.
Finally, I designed calibration circuitry for the analog portions of the chip. I modified a processor that was used for running the calibration process, wrote a macro assembler for the processor and developed a complicated calibration procedure to run on the processor. I also wrote much of the logic that interfaced the processor with the analog circuits.
My work can be found in hard disk drives made by Seagate, Hitachi and Western Digital.
In an effort to encourage the growth of young engineers, I developed a microcontroller development kit called Shorties. This kit was designed to cost under $10 in prototype quantities so that it could be used for "bring your son or daughter to work day" at Agere Systems. The project was funded by Agere Systems with the help of Advanced Circuits. I designed the printed circuit board so that it had seven dual color LEDs on one side so that the board could be spun on a string, making a persistence of vision toy. I also wrote embedded software to implement the persistence of vision toy. To make it more interactive, I wrote desktop software that allowed the kids to draw their own pictures for the board and to download custom programs to the board. The code and design is available on the software page.
I contributed improved interactive routing routines to the FreePCB application. I made routines to that lines would snap to grid lines even if they didn't start on a grid point. Previously the interactive router would only snap to grid points. The code is open source and is available from freepcb.com .
My partner Robert Hasegawa (now a graduate student at University of the Pacific) and I developed a video game console called The Eidolon (a play on the Phantom game console that shockingly never came into existence). I developed a TV controller board using a video DAC, TV encoder and an FPGA. This controller handled all of the double buffering and sprite operations so that software development was extremely easy. I also developed a phase modulation audio synthesis algorithm carefully tuned for maximum performance on a PIC18F microcontroller. The code for this is available on the software page.
I reverse engineered the communication protocol for a Perkin-Elmer phosphorescence spectrofluorometer. The old equipment required a UNIX workstation from the early 1980s to operate and no modern interfaces were developed. I used a serial debugger to monitor the communication across a serial cable and based on the data I captured, I created a GUI in Python that enabled the key functionality from a Windows PC. The code for this is available on the software page.
I started at NVIDIA in the technical marketing department. There I ran performance benchmarks of NVIDIA and competitor products. Because of the tedium of this task, I, along with other engineers, developed a system in Perl to automate the process. When drivers were stable, this system drastically improved the throughput of the team. It allowed a single technician to manage four or more computers simultaneously.
When I returned to NVIDIA for a second internship in 2004, I worked on the mobile hardware team. In addition to my normal tasks of performing power consumption characterization and memory timing configuration, I developed a circuit board and embedded software to carefully control the temperature of a chip under test. The board controlled power to a number of heating elements embedded in a custom designed heat sink that was attached to the chip under test. I developed a model of the system and using the model, developed a PID controller that would hold the temperature of the chip within a few degrees of the target temperature. I also developed functionality for using peltier coolers for cold testing of chips that was not utilized until after I left.
I worked on the infamous GeForce 5800, along with the 5900, 5600, and 5200 products in 2003. When I returned in 2004, I worked on the 6800, 6600, and 6400 mobile products.
I am a teaching assistant for the introductory C programming class for electrical and computer engineers at the University of Colorado at Boulder. I teach one lab section. This experimental course (notes available here) takes an innovative approach to teaching C. Because electrical and computer engineers are likely to be developing embedded software at some point in their careers, this course focuses intensely on understanding C. It starts with memory and pointers and develops functions, recursion, loops and data structures over 10 weeks. It also introduces the students to software engineering with subjects like Makefiles, multiple file projects, abstract data types and unit testing. The remainder of the course teaches students how to use Matlab for numerical computation, culminating with numerical solution to differential equations.
As a teaching assistant, I give additional recitation lectures to emphasize and build upon regular lectures. I hold office hours for students and help them with the difficulties they encounter when code doesn't compile, doesn't work or behaves unexpectedly.
I graded homework, quizzes and exams for the discrete math class. This was an interesting job for me as I never took a discrete math course myself. My university taught digital design in its place. This meant that I was had never really encountered proofs prior to graduate study. This was a very good exercise in paper proofs. I have since started using Coq to redo some of the proofs presented in the discrete math class. These proofs and the use of Coq are discussed on my blog.
My first teaching assistant assignment was Computers as Components. This class is the introduction to assembly language class. I have now taught five labs worth of students over three semesters under three different professors. I taught nearly 100 students the intricacies of Motorola 68k assembly. I helped students understand assembly language, the hardware stack, interrupt processing, data structures, I/O and memory hierarchy through a variety labs. Students developed audio recorders, Morse Code generators, and games.
I also developed a lab where students created a memory hierarchy simulator. Due to the difficult of this task, I created a framework for the students. The framework, written in C++, simulates caches and a translation look- side buffer. While difficult, the lab greatly helped students understand how memory hierarchy worked. The code for the framework is available on the software page.
It should come as no surprise that someone who has developed significant code in Perl, Python, C, C++, a variety of assembly languages, Java, OCaml and Verilog is something of a language nut. I'm an active member of the University of Colorado Programming Languages Group. I have a fascination with parallel programming languages. I'm particularly interested in synchronization and verification and program analysis of parallel programs.
I have played saxophone for longer than I have programmed computers. I almost finished a music minor as an undergraduate. I studied saxophone and music theory, sang with the university choir, performed with the concert band and played with the pep band. The only class I didn't take was music history. I also am a member of the Phi Mu Alpha music fraternity. I learned to appreciate and sing a capalla with this group of extremely talented musicians. My music page has more information about my music pursuits.
My wife, Jennifer O'Brien, and I take weekly ballroom dance lessons from Jes Torres at World of Dance in Denver. While I am not good at it, I have found it to be quite a bit of fun. It presents quite the combination of physical and intellectual challenge.
In 2009, I got my first DSLR camera. While I've owned cameras in the past, a DSLR changed photography for me. In the first year of owning my camera I took more than 20,000 photographs. While most were exceedingly bad, I am learning how to better control the camera and how to get the color and lighting that I want, while maintaining a good composition. See my photography page for some of my pictures.
I started flying in 2009 under the instruction of the talented Brett Sloan. While I possess no great skill here, I find it to be a nice challenge and a fantastic excuse to get outside. Some day it is my goal to develop an unmanned aerial vehicle by automating one of my planes. I doubt this day will come any time soon. I fly a Mountain Models Magpie Sport.