Hi, I am a final year PhD student in computer science at ETH Zurich. My main advisor is Peter Müller and my second advisor is Alex Summers.
I am very interested in the question: How can we develop software programs that are guaranteed to work as intended (for instance, do not crash, compute only correct results, and do not leak sensitive information)? In my PhD, I have been exploring answers to this question using formal program verification techniques, which allow one to formally prove that programs behave as expected. In particular, I have developed program verification techniques, which I have applied to two existing and complex programs that are widely used in the program verification community: Viper and Boogie. Both of these programs are automated program verifiers. That is, they accept as input a program and a specification expressing a property that must be satisfied by executions of the input program. Given such an input, automated program verifiers automatically verify whether executions of the input program indeed satisfy the input specification. That means my research has focused on verifying programs, which themselves verify programs. A distinguishing aspect of my work is that it focuses on existing program verifier implementations used in practice with all their intricacies, instead of considering idealized verifier implementations.
After completing my PhD this year, I am planning to transition from academia to industry, where I would like to work in an environment that values software quality.
My LinkedIn profile is here.
You can contact me at first name.last name@inf.ethz.ch.