Alexander Vaynberg

alv ***at***
Department of Computer Science
Yale University
51 Prospect Street
New Haven, CT 06511 USA

I am a Ph.D. student at the Department of Computer Science of Yale University. My advisor is Zhong Shao and I am a member of the FLINT research group. I have completed my undergraduate studies at Carnegie Mellon university. My research interests are programming languages and software verification.


I think that formally specified and certified software is an important next step in software development. There will be fewer bugs in the code, and it will enable end-users and developers to ensure that software satisfies their requirements, whatever these requirement may be. I am glad to be a part of the research effort that will make this happen.

My research effort focuses on the problem of lack of reusability in formally certified methods. It is my opinion that much of the current attempts at verification result in a one-shot approach, where the entire project is certified against a single specification, with methods that are chosen specifically for this project. Because of the ad-hoc nature of such verification attempts, it is hard to reuse the results.

My current approach to this problem is to define a framework for creation of reusable certified modules. The challenge is to enable each module to be certified independently at its own level of abstraction, and also to provide methods for linking these modules, so that certification of complex systems becomes possible.

The papers about this work are currently in progress. This research also resulted in a trace-based software verification approach, which is worked on by other members of our team.

This research has roots in an earlier work on Certified Assembly Programming, a project where I was a participant. There our group was developing methods for using foundational proof-carrying code techniques to verify assembly code as well as to reason about stack-based workflow these problems presented. My work has helped develop a logic for reasoning with exceptions and non-local jumps. I have also helped with the work on certification of self-modifying code by certifying an operating system bootloader.

Publications that relate to this work are:


I enjoy explaining challenging concepts to people. It is very rewarding to see students gain an understanding of a complicated subject. For this reason, I have an extensive experience of being a teaching assistant for many classes:

Semester Class Name Professor University
Spring 2010 CS 422 Operating Systems Bryan Ford Yale
Fall 2009 CS 421 Compilers and Interpreters Zhong Shao Yale
Spring 2009 CS 112 Intro to Programming Daniel Abadi Yale
Fall 2008 CS 112 Intro to Programming Drew McDermott Yale
Spring 2008 CS 422 Operating Systems Zhong Shao Yale
Fall 2007 CS 421 Compilers and Interpreters Zhong Shao Yale
Spring 2006 CS 422 Operating Systems Zhong Shao Yale
Fall 2005 CS 421 Compilers and Interpreters Zhong Shao Yale
Fall 2003 15-212 Principles of Programming Stephen Brookes Carnegie Mellon

It is unfortunate that almost all the programming that I have done recently has been for research related activities rather than for personal non-scientific interest. Due to my teaching and work, I specialize in functional programming in ML-like languages as well as low-level operating system code written in C and assembly.

My personal programming interests are usually directed towards creation of protocols / interfaces and attempts to make things more general. Here are a few examples I have toyed with, but never had the chance to bring to completion:

Some of these unfinished ideas I hope to restart once I am done with my dissertation.

Leisure I have several diverse hobbies for which I can never find the time. These include biking, mushroom hunting, and Euro-style board games. I am also interested in design of transportation networks, but I do not know how to pursue this interest, except through reading books or an occasional game of Transport Tycoon.