Hi there! I'm Caleb Voss—computer scientist and mathematician. I am a PhD student in programming language theory under Prof. Bill Harris at Georgia Tech. My research is targeting automated proofs of safety properties to make real-world programs dependable. My current activities are primarily focused on shape analysis, that is, reasoning about heap-allocated datastructures. How do you prove that your program's linked list can never have any cycles? Or that no node appears at two different locations in a tree after re-balancing? But here's the twist: you're not allowed to invoke your human intuition or creativity to prove it!

I hope you will find a few cross-sections of my intellectual life on these pages, including further discussion of my research interests and side projects. Feel free to explore!


I have joined the programming languages lab of Prof. Bill Harris at Georgia Tech, pursuing automated proofs of program safety.

I am spending the summer at the University of Kentucky with Prof. Jim Griffioen. We are tackling a cross-domain project that combines high-level programming languages with software-defined networking.

Congratulations to my mentor, Prof. Lydia Kavraki, for winning the Rice University Presidential Mentoring Award! Her support has been invaluable to me.

My undergraduate research at Rice University has been recognized with the James S. Waters Creativity Award and by the Rice Engineering Alumni with the Outstanding Research Excellence Award.

I am pleased to announce that I have been offered an NSF Graduate Research Fellowship! See the Rice CS blog post.