Michael Barnett is a Research Software Design Engineer in the Programming Languages and Methods group, which is part of the Research in Software Engineering (RiSE) team.   I am currently working on 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. For the past several years, I have worked on Spec# (pronounced "speck-sharp"), 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. The other members of the Spec# team are: Manuel Fähndrich, Rustan Leino, Francesco Logozzo, Wolfram Schulte, and Herman Venter.

Home | Biography | Research | ILMerge

This site was last updated 10/21/08