I am 5th (final) year PhD student in the University of Pennsylvania advised by Sebastian Angel and Steve Zdancewic. I work in the reliability, security and privacy of computer systems by combining techniques from formal verification and cryptographic zero-knowledge proofs (zkSNARKs). I believe the two approaches are complementary. I am currently looking for research scientist positions, starting in Fall 2025.

Before starting my PhD I worked for 5 years in industry as a Software Engineer (Bridgewater Associates, Apple) and Tech Lead at UnifyID. I completed by Bachelor’s and Masters in MIT my thesis advisors were Frans Kaashoek and Nickolai Zeldovich. I am from Thessaloniki, Greece and I like hiking, snowboarding and camping.

Confidential communication is not only important, but necessary in plenty of scenarios, from online purchases to communicating military intelligence. In order to achieve trust and confidentiality in communications computer scientists invented cryptographic protocols. While the theory behind cryptographic protocols has been rigorously formalized, their implementations are not and prone to bugs. This space is fertile grounds for formal verification of computer programs, which has had success in both academia and industry[1][2].

In functional languages, algebraic types are an important part of the user experience and the most complete and minimal way to define data structures. In the Coq proof assistant, the polymorphic list definition is inductively defined, here is what it looks like.