Research Papers

2008

• Boogie Meets Regions: A Verification Experience Report
  Anindya Banerjee, Mike Barnett, and David A. Naumann
  MSR-TR-2008-79

2007

• Annotations for (more) Precise Points-to Analysis
  Mike Barnett, Manuel Fähndrich, Diego Garbervetsky and Francesco Logozzo
  IWACO 2007

2005

• Weakest-Precondition of Unstructured Programs
  Mike Barnett and K. Rustan M. Leino
  PASTE 2005
• Boogie: A Modular Reusable Verifier for Object-Oriented Programs
  Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino
  FMCO 2005

2004

• The Spec# Programming System: An Overview
  Mike Barnett, K. Rustan M. Leino and Wolfram Schulte
  CASSIS 2004
• 99.44% pure: Useful Abstractions in Specifications
  Mike Barnett, David A. Naumann, Wolfram Schulte, and Qi Sun
  FTfJP 2004
• Friends Need a Bit More: Maintaining Invariants Over Shared State
  Mike Barnett and David A. Naumann
  MPC 2004
• Towards Imperative Modules: Reasoning about Invariants and sharing of mutable state
  David A. Naumann and Mike Barnett
  LICS 2004

2003

• Verification of Object-Oriented Programs with Invariants
  Mike Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte.
• .NET Contracts: Attaching Specifications to Components
  Mike Barnett, Wolfram Schulte, and Nikolai Tillmann
• Model-Based Testing with AsmL.NET
  Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes
  [PDF]
• Validating Use Cases with the AsmL Test Tool
  Mike Barnett, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes
  [PDF]
• Scenario-Oriented Modeling in AsmL and its Instrumentation for Testing
  Mike Barnett, Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes
  [PDF]
• Towards a Tool Environment for Model-Based Testing with AsmL
  Mike Barnett, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes
  [PDF]
• Serious Specification for Composing Components
  Mike Barnett, Wolfgang Grieskamp, Clemens Kerer, Wolfram Schulte, Clemens Szyperski, Nikolai Tillmann, and Arthur Watson
• Runtime Verification of .NET Contracts
  Mike Barnett and Wolfram Schulte

2001

• The ABCs of Specification: AsmL, Behavior, and Components
  Mike Barnett and Wolfram Schulte
• Spying on Components: A Runtime Verification Technique
  Mike Barnett and Wolfram Schulte
• Conformance Checking of Components Against Their Non-deterministic Specifications
  Mike Barnett, Lev Nachmanson, and Wolfram Schulte

2000

• Using Abstract State Machines at Microsoft: A Case Study
  Mike Barnett, Egon Börger, Yuri Gurevich, Wolfram Schulte, and Margus Veanes.

Research Talks

2004

• Stevens Institute of Technology, Hoboken NJ. October 18 2004.
• Kansas State Univeristy, Manhattan KS. September 22 2004 and September 23, 2004.