Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Mike Barnett

Mike Barnett
PRINCIPAL RSDE
.

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

  • Tempe: An environment for doing interactive data analytics. Check out our video!
  • 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.
  • ILMerge: a static linker for .NET assemblies.

What I Did

  •  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!
Publications