About Me

Hello! I am a Software Engineer based in Austin, Texas and a recent graduate of Boston University's Computer Science program. Before entering the world of Computer Science, I spent most of my time racing bicycles, achieving podiums at National Championships and competing the Canadian National Team. I wrote code for the first time during my Sophomore year of college, but my passion for Computer Science was first ignited by an Introduction to Programming Languages class. This led me to aggressively pursue a curriculum of graduate courses, including a class on Formal Methods.

Next year, I hope to begin my PhD in the area of programming languages. Currently, I am conducting research on Formally Verifying Algorithms for Differential Privacy, with Professor Marco Gaboardi (BU) and Professor Arthur Azevedo De Amorim (RIT). My research interests mainly lie in Formal Verification, along with a keen interest in Type Theory and other light weight formal methods. I am particularly interested in verifying real programs (in existing languages) using Hoare and Separation Logic. Ultimately, I would like my work to directly impact the number of terrifying bugs that exist in code.

Research Interests

Writing correct code can be a difficult task. Initially, I believed that Formal Methods could be the solution to ensuring all software is correct. However, the overhead of performing mechanized mathematical proofs can be too high to achieve such an ambitious goal. As a result, I am deeply interested in finding ways to lower the barriers for engineers to ensure that productionalized code is correct.

In my future research, I aim to work at the intersection of theory and engineering. I strongly believe that great engineering is propelled by theory, but for systems to be effective, the theory must be abstracted away. Thus, my focus is on research that can have an immediate impact on industrial applications. My work on Differential Privacy is an example of this.

Research Oriented Work

CoqPL Talk on Verified Differential Privacy
You can read the extended abstract below.

Verified Differential Privacy for Finite Computers
This extended abstract details part of my work on verifying algorithms for Differential Privacy using the Coq Proof Assistant. I submitted and presented this work at CoqPL 2023. Since then, I have verified two "fast" implementations of the Geometric Mechanism, and am working on verifying a few other DP Mechanisms using a library derived from my original work.

Compositional Secure Compilations
I have done a small amount of proof work on Compositional Secure Compilation. Please check out Matthis Kruse's fantastic work.

A Primer on Property Based Testing for Python - Source Code
PyBT is a python library for property based testing I created, in an effort to get my fellow engineers to use verification-like methods.

RQS
This is a Rust implementation of an AWS SQS style queueing system. Eventually I'd like for this to be a multi-node distributed system with durable and ordered queues.

Heat Adjusted Power
This is not a PL project, but I feel it is worth including. Heat Adjusted Power is the only model that is able to adjust cyclist's effort level for ambient temperature. This site was formally launched as a product by CCNS. Big thanks to Professor Michael Kane (Yale) for his guidance.

More Coming Soon!
I have more projects planned with various faculty in the very near future! Until they start, I will omit them from this page.

Education & Work Experience

Boston University - Computer Science
I graduated with a B.A. in CS from BU in May of 2022.

Dimensional Fund Advisors - Software Engineer
I have been working as a software engineer at DFA since 2022.

Contact

Please, feel free to send me an email at vrindisbacher77 [at] gmail [dot] com