Code Contracts and Pex: Infrastructure for Dynamic and Static Analysis for .NET


July 12, 2010


Thomas Ball, Mike Barnett, Christoph Csallner, and Peli de Halleux



Thomas Ball, Mike Barnett, Christoph Csallner, and Peli de Halleux

Thomas Ball is principal researcher at Microsoft Research where he manages the Software Reliability Research group. Tom received a PhD from the University of Wisconsin–Madison in 1993, was with Bell Labs from 1993 to 1999, and has been at Microsoft Research since 1999. He is one of the originators of the SLAM project, a software model checking engine for C that forms the basis of the Static Driver Verifier tool. Tom’s interests range from program analysis, model checking, testing, and automated theorem proving to the problems of defining and measuring software quality.

Mike Barnett is a research software design engineer in the RiSE group in Microsoft Research. He has been at Microsoft since 1995. He previously worked on the Spec# language and is interested in all things programming language.

Christoph Csallner is an assistant professor in the Computer Science and Engineering Department at the University of Texas at Arlington (UTA). Before joining UTA, he worked for Google and Microsoft Research and received a PhD degree from Georgia Tech. He has received two Distinguished Paper Awards, the first one at the 2006 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA) and the second one at the 2007 IEEE/ACM International Conference on Automated Software Engineering (ASE).

Jonathan “Peli” de Halleux is a senior research software design engineer in the Research in Software Engineering group at Microsoft Research in Redmond, Washington, where he has been since October 2006 working on the Pex project. From 2004 to 2006, he worked in the Common Language Runtime (CLR) as a software design engineer in test in charge of the Just In Time compiler. Before joining Microsoft, he earned a PhD in Applied Mathematics from the Catholic University of Louvain. Earlier, he developed the unit testing framework MbUnit.