Michał Moskal

I'm a researcher at Microsoft Research, Redmond in the RiSE group I was a PhD student at the Computer Science Institute of the University of Wroclaw, Poland, now waiting for the defence.

You can contact me at michal.moskal (at sign) microsoft.com.

Projects I currently work on the VCC project, together with collegues from European Microsoft Innovation Center in Aachen. VCC is a deductive verifier for concurrent C programs. In the past I've been working on (among other things): Nemerle programming language. [WEB] Fx7 Satisfiability Modulo Theories solver. [WEB]

Papers

The BiBTeX file with most of the papers below.

• Satisfiability Modulo Software.  Michał Moskal. PhD thesis. University of Wrocław. Submitted in September 2009.
  [PDF]
• VCC: A Practical System for Verifying Concurrent C.  Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, Stephan Tobies. 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009), to appear. (LNCS 5674). Wolfram's invited talk. The paper to cite for VCC.
  [PDF]
• Programming with Triggers.  Michał Moskal. Satisfiability Modulo Theories workshop 2009, to appear. An updated version, with Axiom Profiler and Z3 Inspector descriptions.
  [Paper/PDF|Slides/PDF]
• HOL-Boogie: An interactive prover-backend for the Verifiying C Compiler.  Sascha Böhme, Michał Moskal, Wolfram Schulte, Burkhart Wolff. Journal of Automated Reasoning, 2009, to appear..
  [PDF]
• VCC: Contract-based Modular Verification of Concurrent C.  Markus Dahlweid, Michał Moskal, Thomas Santen, Wolfram Schulte, Stephan Tobies. Research demo at ICSE 2009
  [PDF]
• A Practical Verification Methodology for Concurrent Programs.  Ernie Cohen, Michał Moskal, Wolfram Schulte, Stephan Tobies. MSR-TR-2009-15
  [PDF]
• A Precise Yet Efficient Memory Model For C.  Ernie Cohen, Michał Moskal, Wolfram Schulte, Stephan Tobies. 4th International Workshop on Systems Software Verification (SSV2009). Later in ENTCS Vol. 254.
  [PDF]
• Verification Condition Splitting.  K. Rustan M. Leino, Michał Moskal, Wolfram Schulte. Draft.
  [PDF]
• Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving.  Stefan Maus, Michał Moskal, Wolfram Schulte.   12th International Conference on Algebraic Methodology and Software Technology, AMAST 2008 (LNCS 5140).
  [PDF]
• Rocket-fast proof checking for SMT solvers.  Michał Moskal. 14th International Conference Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008 [On using term rewriting as an eficient proof engine.]
  [PDF]
• Fx7 or In Software, It Is All About Quantifiers .  Michał Moskal. Satisfiability Modulo Theories Competition 2007, Berlin [Fx7 system description, the solver was second in the AUFLIA division.]
  [PDF]
• Edit & Verify.  Radu Grigore, Michał Moskal. First-order Theorem Proving workshop 2007, Liverpool, UK. [During incremental program verification we get many similar formulas, that need to be proven. We show how to simplify the new ones with respect to the old ones, that are already proven.]
  [PDF]
• Reachability Analysis for Annotated Code .  Mikolas Janota, Radu Grigore, Michał Moskal. Specification and Verification of Component-Based Systems, 2007, Cavtat, Croatia. [On smoke-testing soundness of assumptions in program annotations.]
  [PDF]
• E-Matching for Fun and Profit.  Michał Moskal, Jakub Lopuszanski, Joseph R. Kiniry. Satisfiability Modulo Theories workshop 2007, Berlin. Later in Special SMT 2007 ENTCS issue. [E-matching is used in quantifier instantiation in SMT solvers.]
  [PDF]
• Fx7 Technical report.  Michał Moskal, Jakub Lopszanski. [Outdated.]
  [PDF]
• Type Inference with Deferral.  Michał Moskal. MSc thesis, University of Wrocław, Poland [About type inference for nominal type systems with subtyping, parametric polymorphism and overloading. Submitted on June 27th, 2005.]
  [PDF]