Who I Am

I am a Research Software Design Engineer in the Programming Languages and Methods group, which is part of the Research in Software Engineering (RiSE) team.

I have been with the Microsoft Corporation since July 1995. First, I was a member of the Natural Language Processing Group in Microsoft Research, moving to the Foundations of Software Engineering group in the fall of 1999. I am now a member of the Programming Languages and Methods group. Before coming to Microsoft, I had been an assistant professor of Computer Science at the University of Idaho for three years. I received my PhD in Computer Science from the University of Texas at Austin in 1992.

What I Do

Code Contracts: a language-agnostic way to express specifications in .NET languages. Specifications include method preconditions, postconditions, and object invariants. Code Contracts capture programmer intentions about how methods and data are to be used. It is Design-by-Contract meets .NET.
Spec#: an experimental extension to C# that adds design-by-contract features. The Spec# compiler emits run-time checks that enforce the contracts and the Spec# program verifier uses theorem-proving technology to statically check the consistency between a program and its contracts. Spec# helps programmers write correct software and makes explicit the correct usage of APIs for clients. It is integrated into Visual Studio .NET.
ILMerge: a static linker for .NET assemblies.

Publications

Michael Barnett, Manuel Fahndrich, Francesco Logozzo, Peli de Halleux, and Nikolai Tillmann, Exploiting the Synergy between Automated-Test-Generation and Programming-by-Contract, in Proc. 31st International Conference on Software Engineering (ICSE'2009) , IEEE, May 2009
Mike Barnett, Manuel Fahndrich, and Francesco Logozzo, Foxtrot and Clousot: Language Agnostic Dynamic and Static Contract Checking for .NET, no. MSR-TR-2008-105, August 2008
Mike Barnett and David A. Naumann, Boogie Meets Regions: a Verification Experience Report, no. MSR-TR-2008-78, May 2008
Anindya Banerjee, Mike Barnett, and David A. Naumann, Boogie Meets Regions: a Verification Experience Report (extended version), no. MSR-TR-2008-79, May 2008
Mike Barnett, Manuel Fahndrich, Diego Garbervetsky, and Francesco Logozzo, Annotations for (more) Precise Points-to Analysis, in IWACO 2007, 2007
Michael Barnett, David A. Naumann, Wolfram Schulte, and Qi Sun, Allowing State Changes in Specifications, in ETRICS, Springer, 2006
Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino, Boogie: A Modular Reusable Verifier for Object-Oriented Programs, in FMCO 2005, 2005
Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes, Towards a Tool Environment for Model-Based Testing with AsmL, in FATES 2003, Springer Verlag, 2004
Mike Barnett, Rob DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte, Verification of Object-Oriented Programs With Invariants, in Formal Techniques for Java-like Programs (FTfJP), July 2003
Michael Barnett, Wolfram Schulte, and Nikolai Tillmann, Using AsmL for Runtime Verification, in Abstract State Machines, Advances in Theory and Practice, 10th International Workshop, ASM 2003, Springer Verlag, March 2003
Mike Barnett, Wolfram Schulte, and Nikolai Tillmann, .NET Contracts: Attaching Specifications to Components, in Practical Foundations of Business System Specifications, pp. 83–98, Springer Verlag, 2003
Michael Barnett, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes, Validating Use-Cases with the AsmL Test Tool, in QSIC, IEEE Computer Society, 2003
Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes, Model-Based Testing with AsmL .NET, in 1st European Conference on Model-Driven Software Engineering, 2003
Mike Barnett and Wolfram Schulte, Spying on Components: A Runtime Verification Technique, in Workshop on Specification and Verification of Component-Based Systems, October 2001