@inproceedings{MPC2004,
  AUTHOR = "Mike Barnett and David Naumann",
  title = {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},
  booktitle = {MPC},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3125},
  year      = {2004},
  isbn      = {3-540-22380-0},
  pages = {54--84},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{Barnett:Using,
AUTHOR = "Mike Barnett and Egon B{\"o}rger and Yuri Gurevich and Wolfram Schulte and Margus Veanes",
TITLE = "Using {A}bstract {S}tate {M}achines at {M}icrosoft: A Case Study",
BOOKTITLE = "Abstract State Machines: Theory and Applications",
SERIES = "LNCS",
VOLUME = "1912",
PAGES = {367-379},
MONTH = "March",
PUBLISHER = "Springer-Verlag",
ADDRESS = "Berlin, Germany",
YEAR = {2000}
}
 

@TechReport{Barnett-Nachmanson-Sculte01, Key={Barnett \& Schulte},
AUTHOR = "Mike Barnett and Lev Nachmanson and Wolfram Schulte",
Title="Conformance Checking of Components Against Their Non-deterministic Specifications",
Month=Jun,
Year=2001,
Institution="Microsoft Research",
Number="MSR-TR-2001-56",
note = {Available from \verb+http://research.microsoft.com/pubs+}
}
 

@InProceedings{Barnett-Schulte01a,
AUTHOR = "Mike Barnett and Wolfram Schulte",
title = "Spying on Components: A Runtime Verification Technique",
booktitle = "Workshop on Specification and Verification of Component-Based Systems",
editor = "Gary T. Leavens and Murali Sitaraman and Dimitra Giannakopoulou",
month = "Oct.",
year = "2001",
note = "Published as Iowa State Technical Report 01-09a"
}
 

@ARTICLE{Barnett-Schulte01,
AUTHOR = "Mike Barnett and Wolfram Schulte",
title = "The {ABC}s of Specification: {AsmL}, Behavior, and Components",
journal = "Informatica",
month = "Nov.",
year = "2001",
volume = 25,
number = 4,
pages = {517--526}
}
 

@TechReport{Barnett-Schulte02a,
AUTHOR = "Mike Barnett and Wolfram Schulte",
TITLE = "Contracts, Components and their Runtime Verification on the {.NET} Platform",
Month=Apr,
Year=2002,
Institution="Microsoft Research",
Number="MSR-TR-2002-38",
note = {Available from \verb+http://research.microsoft.com/pubs+}
}

@ARTICLE{Barnett-Schulte02b,
author = "Mike Barnett and Wolfram Schulte",
title = "Runtime Verification of {.NET} Contracts",
journal = "The Journal of Systems and Software",
publisher = "Elsevier",
year = 2003,
vol = 65,
number = 3,
pages = {199--208}
}

@InProceedings{Barnett-etal03a,
AUTHOR = "Mike Barnett and Wolfgang Grieskamp and Clemens Kerer and
Wolfram Schulte and Clemens Szyperski and Nikolai Tillmann and Arthur Watson",
title = "Serious Specification for Composing Components",
booktitle = "Proceedings of the 6th ICSE Workshop on Component-Based Software Engineering: Automated Reasoning and Prediction",
editor = "Ivica Crnkovic and Heinz Schmidt and Judith Stafford and Kurt Wallnau",
month = "May",
year = "2003"
}
@INPROCEEDINGS{Barnett-Schulte-Tillmann03,
AUTHOR = "Mike Barnett and Wolfram Schulte and Nikolai Tillmann",
title = "{.NET} Contracts: Attaching Specifications to Components",
booktitle = "Practical Foundations of Business System Specifications",
editor = "Haim Kilov and Kenneth Baclawski",
year = "2003",
pages = {83--98},
ISBN = "1-4020-1480-5"
}
@InProceedings{Barnett-etall03b,
AUTHOR = "Mike Barnett and Rob DeLine and Manuel Fähndrich and K. Rustan M. Leino and
Wolfram Schulte",
title = "Verification of Object-Oriented Programs With Invariants",
booktitle = "Formal Techniques for Java-like Programs (FTfJP)",
editor = "Susan Eisenbach and Gary T. Leavens and Peter Müller and Arnd Poetzsch-Heffter and Erik Poll",
month = "July",
year = "2003",
note = "Published as Technical Report 408 from ETH Zurich."

}