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.
- Michael Barnett, Mehdi Bouaziz, Manuel Fahndrich, and Francesco Logozzo, A case for static analyzers in the cloud, in Bytecode 2013, , March 2013
- Patrick Cousot, Radhia Cousot, Francesco Logozzo, and Mike Barnett, An Abstract Interpretation Framework for Refactoring with Application to Extract Methods with Contracts, in Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12), ACM SIGPLAN, 23 October 2012
- Francesco Logozzo, Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Mike Barnett, A Semantic Integrated Development Environment, in Companion of the Proceedings of the to the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2012), ACM SIGPLAN, October 2012
- 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
- 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, 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 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, 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
- 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
- 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, 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, Wolfram Schulte, and Nikolai Tillmann, .NET Contracts: Attaching Specifications to Components, in Practical Foundations of Business System Specifications, pp. 83–98, Springer Verlag, 2003