@Article{Boehme:JAR2009,
  author = {Sascha B\"ohme and Micha{\l} Moskal and Wolfram Schulte and Burkhart Wolff},
  title = {{HOL}-{B}oogie --- An Interactive Prover-Backend for the {V}erified {C} {C}ompiler},
  journal = {Journal of Automated Resoning (JAR)},
  year = 2009,
  doi = {10.1007/s10817-009-9142-9},
  pdf = {http://www.lri.fr/~wolff/papers/journals/hol-boogie.pdf}
}

@InProceedings{Cohen:SSV2009,
  author =       "Ernie Cohen and Micha{\l} Moskal and Wolfram Schulte
                 and Stephan Tobies",
  title =        "A Precise Yet Efficient Memory Model for {C}",
  pages =        "85--103",
  booktitle =    "4th International Workshop on Systems Software
                 Verification (SSV 2009)",
  year =         "2009",
  publisher =    "Elsevier Science B.V.",
  series =       "Electronic Notes in Theoretical Computer Science",
  volume =       "254",
  ee =           "http://dx.doi.org/10.1016/j.entcs.2009.09.061",
}

@InProceedings{Cohen:TPHOLs2009,
  author =       "Ernie Cohen and Markus Dahlweid and Mark Hillebrand
                 and Dirk Leinenbach and Micha{\l} Moskal and Thomas
                 Santen and Wolfram Schulte and Stephan Tobies",
  title =        "{VCC}: {A} Practical System for Verifying Concurrent
                 {C}",
  booktitle =    "Theorem Proving in Higher Order Logics (TPHOLs 2009)",
  address =      "Munich, Germany",
  year =         "2009",
  publisher =    "Springer",
  series =       "Lecture Notes in Computer Science",
  volume =       "5674",
  note =         "Invited paper, to appear.",
}
@InProceedings{Maus:AMAST2008,
  author =       "Stefan Maus and Micha{\l} Moskal and Wolfram Schulte",
  title =        "{Vx86}: {x86} Assembler Simulated in {C} Powered by
                 Automated Theorem Proving",
  month =        jul,
  year =         "2008",
  pages =        "284--298",
  editor =       "Jos{\'e} Meseguer and Grigore Ro{\c s}u",
  booktitle =    "Algebraic Methodology and Software Technology (AMAST 2008)",
  address =      "Urbana, IL, USA",
  publisher =    "Springer",
  series =       "Lecture Notes in Computer Science",
  volume =       "5140",
  ee =           "http://dx.doi.org/10.1007/978-3-540-79980-1_22",
}

@TechReport{Cohen:MSR-TR-2009-15,
  author =	 {Ernie Cohen and Micha{\l} Moskal and Wolfram Schulte and Stephan Tobies},
  title =	 {A Practical Verification Methodology for Concurrent Programs},
  institution =	 {Microsoft Research},
  year =	 2009,
  number =	 {MSR-TR-2009-15},
  month =	 feb,
  note =	 {Available from
                  \url{http://research.microsoft.com/pubs}}
}

@Article{Moskal:E-matching,
  author    = {Micha{\l} Moskal and
               Jakub {\L}opusza{\'n}ski and
               Joseph R. Kiniry},
  title     = {E-matching for Fun and Profit},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {198},
  number    = {2},
  year      = {2008},
  pages     = {19-35},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2008.04.078},
}


@InProceedings{Moskal:TACAS2008,
  author    = {Micha{\l} Moskal},
  title     = {Rocket-Fast Proof Checking for SMT Solvers},
  year      = {2008},
  pages     = {486-500},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4963},
  ee        = {http://dx.doi.org/10.1007/978-3-540-78800-3_38},
  booktitle = {Tools and Algorithms for the Construction and Analysis of
               Systems, 14th International Conference, TACAS 2008}
}

@InProceedings{Moskal:SMT2009,
  author    = {Micha{\l} Moskal},
  title     = {Programming with Triggers},
  year      = {2009},
  booktitle = {Satisfiability Modulo Theories Workshop 2009}
}