A programmer’s progress: Michał Moskal’s journey
By: Futures
Tags: Career Choices, education, ICT studies, New skills for jobs, Skills for innovation
01 December 2009
How a student from Wrocław became an expert in software verification – via Aachen and Redmond.
Today’s software is incredibly complex – and the source code leaves no room for ambiguity. That calls for new tools to express, test and verify the desired design and behaviour of a program. This is where Michal Moskal comes in. At EMIC, the European Microsoft Innovation Center in Aachen, Germany, he’s helping to develop formal software verification to a new level. He works on merging mathematics, in particular proofs of logical theorems, with engineering best practices. Futures talked with him about his journey from Wroclaw University in Poland to the research labs of Microsoft.
FUTURES: How did you meet Microsoft?
Michal Moskal: We, that is a handful of master’s students at Wroclaw University in Poland, got a €25,000 grant for our work on a programming language called Nemerle. We were actually quite surprised. We knew that we did a decent job, designing the language and implementing the compiler, but it is one thing to be happy about what you’re doing and another to have somebody else – and hey, not just somebody else, but the largest software company in the world – recognise that. This was the first grant awarded by Microsoft for academic activity in Poland. It was quite an experience. Press interviews, even one on national TV.
F: Was Microsoft’s .NET-Platform a milestone in your programmer’s life?
MM: In Wroclaw, and I think at almost all excellent universities, students get indoctrinated, right from the first year, that functional programming is the way to go – even if mainstream programmers don’t use it, probably should say not yet. You know, the kind of programming where instead of thinking of updating the state of a computer you think of evaluating a gigantic expression. Then, there is .NET. You can run different programming languages on top of this platform – they can talk to each other. It is not supposed to be tied to one specific language. Microsoft also proposed openness and the platform to be standardised; there was also an open-source implementation of this platform in the works, Mono. This was a major factor, at least for me.
We thought that this .NET platform would clearly benefit from a proper functional language that would give full and convenient access to all the platform’s features. So why not design a new language? And that was the one we later called Nemerle.
F: Where has your recent research been going?
MM: In 2004 I got my MSc and started my PhD. I took Nemerle and started developing a Satisfiability Modulo Theories (SMT) solver in it. SMT solvers take a logical formula and look for a model. Imagine a “world”, where the formula is true: so you can ask, does there exist a model where x
Software verification tasks can be translated into those large formulas. There were quite a few such solvers around already. Most were quite new, but surprisingly, most people were still using the ten-year-old Simplify system for software verification. And in that area, ten years was like ages. So I developed a new solver based on Nemerle.
Michal Moskal, European Microsoft Innovation Center, loves to quote the famous Dutch computer scientist Edsger Dijkstra, who used to say about software verification that “testing is very effective at finding bugs, but is hopelessly inadequate for showing their absence.” He also likes hiking in the high mountains of the Pacfic Northwest.
F: So how did you arrive at Microsoft?
MM: In the SMT community you work with benchmarks. You have a large number of logical formulas that other people have constructed, and you let your solver prove them. There is even a worldwide annual competition. The more problems your solver proves, the better.
So, I was asking around for more benchmarks, among others sending an email to the mailing list of the Spec# team at Microsoft Research. Spec# is an evolution of the programming language C#, supporting formal verification, being developed at Microsoft Research in Redmond, USA. Rustan Leino from Microsoft Research asked me whether I wanted to apply for an internship to work on an SMT solver. I applied and passed the interview.
Microsoft Research is a great place.
You get paid good money for working on interesting problems, like beating Simplify [he smiles]. It’s much like academic research, but you don’t have teaching duties.
F: Where is your work heading to?
MM: SMT solvers are very important for software verification. For example, you ask the solver, “Is there a world where my program crashes?” You “just” need to formally verify it, i.e. prove a mathematical theorem, which is equivalent to your program being correct. This is great, much better than testing. You are mathematically proving there are no bugs. The famous Dutch computer scientist Edsger Dijkstra said that testing is very effective at finding bugs, but is hopelessly inadequate for showing their absence.
F: Today you are working in Verisoft, a collaborative project with a global team...
MM: Back in Europe, I spent a couple of months at University College in Dublin. After a few months in such a flat place as Ireland I wanted to see the mountains again. And the Pacific Northwest is one of the best places for hiking. You’re right on the seaside, but at the same time out of your window you can see a 4,400-metre stratovolcano, or actually a few of them, the Cascades! That really makes you eager for the weekend.
So I thought, maybe they would want me for another internship – challenging problems, hiking, and some money for a poor graduate student. I asked people I got to know at Microsoft Research, and it turned out that they were just starting this huge collaborative project, Verisoft/XT, to verify the Windows Hypervisor software. And they needed someone to build the verification tools, which meant translating C program code into SMT formulas.
The Hypervisor verification is a collaborative project, with Microsoft Research and the Microsoft Windows group working with partners in Germany: EMIC in Aachen, DFKI (German Centre for Artificial Intelligence) and Saarland University.
I decided to spend time working in Aachen, thus being able to visit the Wroclaw University every now and then to get my PhD done. My PhD thesis was aligned with my work at Microsoft, so I could reuse papers I’ve published. See www.verisoft.de/PublicationPage.html
EMIC turned out to be a really nice place. I liked the skew towards applied research. I somehow always end up somewhere on the edge of theory and practice, trying to turn one into the other, and this is what I could do at EMIC. The result of my work at EMIC is the VCC tool (see Box). I am moving to Microsoft Research in the US, looking forward to tackling new challenges.
Background briefing
Verisoft XT – a German research project
Verisoft XT is a three-year research project funded by the German Federal Ministry of Education and Research (BMBF). Its goal is the pervasive formal verification of computer systems and showing the correctness of the systems’ functionality. The correctness proof is reached through mathematical and computer-aided tools in interaction with human input.
As part of this project, the European Microsoft Innovation Center, the German Research Center for Artificial Intelligence and the University of the Saarland, Saarbrücken, set out to prove the correctness of the Microsoft Hyper-V virtualisation kernel – 100,000 lines of C code. Now, two years later, substantial parts of the hypervisor kernel have been verified and some subtle bugs have been found that, so far, had escaped the rigorous testing discipline of the product group.
At the core of the effort is Microsoft’s verification tool for concurrent C, called VCC, developed jointly by EMIC and Microsoft Research, Redmond, USA. VCC can now be downloaded for non-commercial use from vcc.codeplex.com. The project has shown that, after 40 years of research, verification of commercial software is at last feasible.
European Microsoft Innovation Center
The European Microsoft Innovation Center (EMIC), founded in 2003 in Aachen, Germany, is a Microsoft Research & Development facility. It focuses on collaborative applied research in Europe. EMIC works in the context of development programmes sponsored by the European Commission and the German Ministry of Education and Research. Its research focuses on enterprise, mobility, home, security, software verification and embedded systems.
http://microsoft.com/EMIC