About
Research
My current research interests lie in logics for sequences and their applications to computer science. In particular, my current main research line is on an in-depth analysis of specifications languages for programs manipulating unbounded data structures. Using results from classical model theory I describe logical fragments with reasonable decision complexity and I investigate automated reasoning techniques such as combination of theories or interpolation which makes these fragments applicable in various software verification scenarios. In my work, I have 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.