About
Research
My current research interests lie in the interaction between decision procedures and learning algorithms in the context of logics of sequences.Previously, I investigated decision procedures for logics of sequences. In particular, my main research goal was to perform an in-depth analysis of specifications languages for programs manipulating unbounded data structures. Using results from classical model theory I described logical fragments with reasonable decision complexity and I investigated automated reasoning techniques such as combination of theories or interpolation which makes these fragments applicable in various software verification scenarios. In my work, I repeatedly found that supporting componentwise specifications is both a useful and relatively unexplored area of research.
I also have experience with the design of software verifiers and the use of proof assistants. Some of the proofs I wrote in Isabelle are available in the Archive or Formal Proofs and I even wrote a paper about one of them together with Thomas Hales. In particular, the Isabelle proof of the group law of Edwards curves is an example of the power of modern formal methods tools.