Who I Am

I am a Research Software Design Engineer in the Research in Software Engineering (RiSE) group.

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 Research in Software Engineering (RiSE) 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 any .NET language. Specifications include method preconditions, postconditions, and object invariants. Code Contracts capture programmer intentions about how methods and data are to be used. In .NET 4.0, the Contract class is part of the Base Class Library! In order to use contracts, you need to go to DevLabs and download the tools that provide runtime checking, static checking, and documentation generation. Try it out and give your feedback in order to shape the future of .NET!
CCI: The Common Compiler Infrastructure is the framework to use if you are doing anything related to .NET binaries, either creating them from scratch, modifying existing ones, or just mining them for information.
Spec#: an experimental extension to C# that adds contract features such as method pre- and postconditions and object invariants. It also has a non-null type system. 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. And now it is available as an open source project!
ILMerge: a static linker for .NET assemblies.

Projects

Publications

Manuel Fahndrich, Michael Barnett, Daan Leijen, and Francesco Logozzo, Integrating a Set of Contract Checking Tools into Visual Studio, in Proceedings of the 2012 Second International Workshop on Developing Tools as Plug-ins (TOPI 2012), IEEE, 3 June 2012
Mike Barnett, Manuel Fahndrich, K. Rustan M. Leino, Peter Mueller, Wolfram Schulte, and Herman Venter, Specification and Verification: The Spec# Experience, in Communications of the ACM, vol. 54, no. 6, pp. 81--91, Association for Computing Machinery, Inc., June 2011
Mike Barnett and K. Rustan M. Leino, To Goto Where No Statement Has Gone Before, in VSTTE 2010, August 2010
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 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, Robert DeLine, Bart Jacobs, Manuel Fahndrich, Rustan Leino, Wolfram Schulte, and Herman Venter, The Spec# programming system: Challenges and directions., in Verified Software: Theories, Tools, Experiments (LNCS4171, ISSN 0302-9743), Springer Verlag, 10 October 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 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, 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 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
Editors, Jim Davies, Wolfram Schulte, and Mike Barnett, Formal Methods and Software Engineering, 6th International Conference on Formal Engineering Methods, ICFEM 2004, Springer Verlag, 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, 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
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
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