Michal is a PhD student at the Computer Science Institute of the University of Wroclaw, Poland. He also works at the European Microsoft Innovation Center on the Verifying C Compiler project, among other things. He used to be a PLD Linux developer, leader of the Nemerle project and the sole developer of Fx7 SMT solver. He visited our group for a few very productive months in Summer 2007. During that time he co-wrote several research papers with group members, contributed to the development of several tools, and gave a talk about his theorem prover, Fx7.