my photo

michał.moskal

michal.moskal(@)microsoft.com

Michał Moskal works at Microsoft Research in Redmond on software verification, automated theorem proving, and programming languages. During his MSc and later PhD studies at the University of Wrocław in Poland he had led development of Nemerle—a high-level programming language for the .NET platform, and (using Nemerle) Fx7—a satisfiability modulo theories (SMT) solver.

While finishing the PhD he joined European Microsoft Innovation Center in Aachen in early 2008 and was instrumental to development of VCC—a formal verifier for concurrent C programs utilizing SMT technology. VCC represents the state of the art in semi-automatic C verification and has been used on tens of thousands of lines of industrial C code.

In late 2009, after receiving the PhD degree with honors and prime minister award, Michał has moved to the RiSE group at Microsoft Research Redmond and continued to work on VCC while also taking on other projects including Boogie intermediate verification language, SPUR tracing JIT, and DKAL authorization engine. In late 2010, Nikolai Tillmann and Michał have started TouchDevelop—an effort to create an integrated development environment for writing programs directly on touch-enabled mobile devices (particularly phones and tablets).

short version

Michał Moskal works at Microsoft Research in Redmond on software verification, automated theorem proving, and programming languages. While working on his PhD degree at the University of Wrocław in Poland he developed Nemerle (a high-level programming language for the .NET platform) and Fx7 (a satisfiability modulo theories (SMT) solver). In 2008 he joined European Microsoft Innovation Center in Aachen, Germany and was instrumental to development of VCC—a state of the art SMT-based verifier for concurrent C programs applied to tens of thousands of lines of industrial C code. Michał continued work on VCC after his 2009 move to Microsoft Research Redmond. In late 2010, Nikolai Tillmann and Michał have started TouchDevelop—an effort to create an integrated development environment for writing programs directly on touch-enabled mobile devices (particularly phones and tablets).

pictures

Hi-res picture :: Med-res picture ::

Back to homepage.