Malte Schwerhoff

About me

Since 2011 I am a doctoral student at ETH, where I also received my Master's. I did my Bachelor's at the FH Gelsenkirchen, during which I spent a great semester abroad at the TPU in Tomsk, Russia. Before going to university I completed an apprenticeship as a media designer. A slightly outdated CV is available.

Areas of research

In the course of my Master's thesis I implemented a symbolic-execution-based verifier for Chalice - called Syxc - which I plan to release eventually. I am also working on (observational) immutability and disjointness and on the specification of actor-based systems.

A snapshot of Syxc and Chalice is available, including several examples from the Chalice test suite that can be used to benchmark the behaviour of the two verifiers.

Publications

I. T. Kassios and P. Müller and M. Schwerhoff: Comparing Verification Condition Generation with Symbolic Execution: an Experience Report
Verified Software Theories Tools Experiments (VSTTE), 2012. [PDF] [BIB] Springer-Online

Teaching

• Formal Methods and Functional Programming (SS 2012)
  
• Informatik für Mathematiker und Physiker (AS 2011)
• Formal Methods and Functional Programming (SS 2010)

Student supervision

Current

• Roland Meyer (B.Sc.) - Developing a common Web Interface to various Verification Tools [PDF]
• Ivo Colombo (M.Sc,) - Debugging Symbolic Execution [PDF]
• Rokas Matulis (M.Sc.) - Extensible Code Contracts for Scala [PDF]