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.

Projects

Publications

Mike Barnett, Manuel Fahndrich, and Francesco Logozzo, Embedded Contract Languages, in ACM SAC - OOPS, Association for Computing Machinery, Inc., March 2010
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
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 and David A. Naumann, Boogie Meets Regions: a Verification Experience Report, no. MSR-TR-2008-78, 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, K. Rustan M. Leino, and Wolfram Schulte, The Spec# Programming System: An Overview, in CASSIS 2004, Construction and Analysis of Safe, Secure and Interoperable Smart devices, Springer, 2005
Mike Barnett and K. Rustan M. Leino, Weakest-precondition of unstructured programs, in PASTE '05: The 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, ACM Press, New York, NY, USA, 2005
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 and David A. Naumann, Friends Need a Bit More: Maintaining Invariants Over Shared State, in Seventh International Conference on Mathematics of Program Construction (MPC 2004), Springer-Verlag, July 2004
Mike Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte, Verification of object-oriented programs with invariants, in Journal of Object Technology, vol. 3, no. 6, pp. 27-56, Technical report 408, Department of Computer Science, ETH Zurich, June 2004
David A. Naumann and Mike Barnett, Towards Imperative Modules: Reasoning about Invariants and Sharing of Mutable State, in Logic in Computer Science (LICS), IEEE, 2004
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 and David Naumann, Friends Need a Bit More: Maintaining Invariants Over Shared State", editor = Dexter Kozen and Carron Shankland, booktitle = Mathematics of Program Construction, 7th International Conference, MPC 2004, Stirling, Scotland, UK, July 12-14, 2004, Proceedings, , 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
Mike Barnett, Wolfgang Grieskamp, Clemens Kerer, Wolfram Schulte, Clemens Szyperski, Nikolai Tillmann, and Arthur Watson, Serious Specification for Composing Components, in Proceedings of the 6th ICSE Workshop on Component-Based Software Engineering: Automated Reasoning and Prediction, May 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
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, Wolfram Schulte, and Nikolai Tillmann, .NET Contracts: Attaching Specifications to Components, in Practical Foundations of Business System Specifications, pp. 83–98, Springer Verlag, 2003
Mike Barnett and Wolfram Schulte, Runtime Verification of .NET Contracts, in The Journal of Systems and Software, no. 3, pp. 199–208, Elsevier, 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, The ABCs of Specification: AsmL, Behavior, and Components, in Informatica, vol. 25, no. 4, pp. 517–526, November 2001
Mike Barnett and Wolfram Schulte, Spying on Components: A Runtime Verification Technique, in Workshop on Specification and Verification of Component-Based Systems, October 2001