Konstantinos Kallas


I am a PhD student at the University of Pennsylvania, where I am fortunate to be advised by Rajeev Alur. My research interests lie in the intersection of programming languages, distributed systems, and software verification. I am particularly interested in ways of making distributed system development more reliable and secure.

Short Bio

I spent the summer of 2019 in the Automated Reasoning Group at Amazon Web Services under the supervision of Daniel Schwartz-Narbonne. We used the C Bounded Model Checker (CBMC) to verify that certain critical C libraries (aws-c-common, aws-esdk-c) are memory safe and satisfy important functional correctness properties. In the process, I implemented several small extensions for CBMC, mostly focused on improving the support for function contracts.

Before my PhD, I was an undergraduate student at the National Technical University of Athens, department of Electrical and Computer Engineering. I completed my thesis “HiPErJiT: A Profile-Driven Just-in-Time Compiler for Erlang based on HiPE” under the supervision of Kostis Sagonas. It is available online in both English and Greek.

In May of 2018 I participated in the Eighth Summer School on Formal Techniques that took place in Atherton, California and was organized by SRI International.

Throughout my undergraduate studies I have developed software for many projects with my colleagues. Some notable examples are a complete compiler for the language Edsger (source), an implementation of the Chord protocol (source), and an extension of the SIP Communicator (source).

I have also participated in Google Summer of Code 2017, where I worked with Evgeny Khramtsov to extend ejabberd. I implemented a mechanism that allows for certificate acquiring through the ACME protocol.







In my free time I enjoy programming (for fun or in programming competitions), board games, escape rooms, and ping pong. I also occasionally play guitar in an amateur jam band.