Dresden, Saxony, Germany
I am working on formal verification of microkernel virtualisation-based security platform. I led a verification effort on ARM system register emulation. As a part of this role, I am contributing to development of formal C++ semantics.
I was investigating properties of Partial Commutative Monoids and the associated notions of structure-preserving morphisms and relations for applications to verification of concurrent algorithms. I was member of Alex Nanevski's research group and I contributed to development of FCSL concurrent separation logic.
I was worked on verification of safety and security of AI applications and I collaborated on verification of planning languages through proof-carrying code -proof carrying plans.
I was collaborating on design and development of enterprise web applications (intranet, extranet, BI) for retail customers. These were built on MS SharePoint platform using C#.