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.
From September to December 2013 I'll be a visiting scholar at the KU Leuven in the group of Bart Jacobs.
In the course of my Master's thesis I implemented a symbolic-execution-based verifier for Chalice - called Syxc - which in the meantime has been superseded by Silicon, which basically is Syxc for Sil, an intermediate verification language we developed in our group. I am also working on (observational) immutability and disjointness and on the specification of actor-based systems.
An outdated 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.
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] [Slides] [BIB] Springer-Online
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to a newer browser.