papers/talks

michał.moskal

papers

A BiBTeX file with most of the papers below.

• Jacdac: Service-based Prototyping of Embedded Systems
  Thomas Ball, Peli de Halleux, James Devine, Steve Hodges, Michal Moskal MSR-TR-2023-4 | January 2023
  [pdf]
• Plug-and-play Physical Computing with Jacdac
  James Devine, Michal Moskal, Peli de Halleux, Thomas Ball, Steve Hodges, Gabriele D’Amone, David Gakure, Joe Finney, Lorraine Underwood, Kobi Hartley, Paul Kos, Matt Oppenheim Proceedings of the ACM on Interactive, Mobile, Wearable and Ubiquitous Technologies | 2022. Vol 6(3)
  [pdf]
• Web-based Programming for Low-cost Gaming Handhelds
  Michal Moskal, Peli de Halleux, Thomas Ball, Abhijith Chatra, James Devine, Steve Hodges, Shannon Kao, Richard Knoll, Galen Nickel, Jacqueline Russell, Joey Wunderlich, Daryl Zuniga Foundations of Digital Games. 2021. Best paper.
  [pdf]
• Rethinking the Runway: Using Avant-Garde Fashion To Design a System for Wearables
  Teddy Seyed, James Devine, Joe Finney, Michal Moskal, Peli de Halleux, Steve Hodges, Thomas Ball, Asta Roseway Proceedings of the 2021 CHI Conference on Human Factors in Computing Systems (CHI '21)
  [pdf]
• The BBC micro:bit: from the U.K. to the world
  Jonny Austin, Howard Baker, Thomas Ball, James Devine, Joe Finney, Peli de Halleux, Steve Hodges, Michal Moskal, Gareth Stockdale Communications of the ACM | February 2020, Vol 63(3)
  [pdf]
• Microsoft MakeCode: Embedded Programming for Education, in Blocks and TypeScript
  Thomas Ball, Abhijith Chatra, Peli de Halleux, Steve Hodges, Michal Moskal, Jacqueline Russell SPLASH-E 2019: Proceedings of the 2019 ACM SIGPLAN Symposium on SPLASH-E. 2019.
  [pdf]
• Static TypeScript: An Implementation of a Static Compiler for the TypeScript Language
  Michal Moskal, Thomas Ball, Peli de Halleux Managed Programming Languages and Runtimes. 2019.
  [pdf]
• MakeCode and CODAL: intuitive and efficient embedded systems programming for education
  James Devine, Joe Finney, Peli de Halleux, Michał Moskal, Tom Ball, Steve Hodges 19th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems. 2018.
  [pdf]
• Beyond Open Source: The TouchDevelop Cloud-based Integrated Development and Runtime Environment
  Thomas Ball, Sebastian Burckhardt, Jonathan de Halleux, Michał Moskal, Jonathan Protzenko and Nikolai Tillmann. MOBILESoft 2015.
  [pdf]
• Gauging Research in Program Synthesis with a Massive Open Online Contest
  Takuya Akiba, Kentaro Imajo, Hiroaki Iwami, Yoichi Iwata, Toshiki Kataoka, Naohiro Takahashi, Michał Moskal and Nikhil Swamy. Draft
  [pdf]
• Tap Here: A Diff-powered Programming Tutorial Engine
  Michał Moskal, Nikolai Tillmann, Jonathan de Halleux, Sebastian Burckhardt, Thomas Ball, and Judith Bishop. 2nd Workshop on Programming Languages Technology for Massive Open Online Courses. PLOOC 2014
  [pdf]
• Exposing Native Device APIs to Web Apps
  Arno Puder, Nikolai Tillmann, and Michał Moskal. Proceedings of First ACM International Conference on Mobile Software Engineering and Systems. (MOBILESoft 2014).
  [pdf]
• Refactoring Local to Cloud Data Types for Mobile Apps
  Michael Hilton, Arpit Christi, Danny Dig, Michał Moskal, Sebastian Burkhardt, and Nikolai Tillman. Proceedings of First ACM International Conference on Mobile Software Engineering and Systems. (MOBILESoft 2014).
  [pdf]
• Addressing JavaScript JIT engines performance quirks: A crowdsourced adaptive compiler
  Rafael Auler, Edson Borin, Peli de Halleux, Michał Moskal and Nikolai Tillmann. 2014 International Conference on Compiler Construction (CC 2014)
  [pdf]
• Co-induction Simply: Automatic Co-inductive Proofs in a Program Verifier
  K. Rustan M. Leino and Michał Moskal. 19th International Symposium on Formal Methods (FM 2014) and Microsoft Research Technical Report MSR-TR-2013-49 (older, extended version)
  [pdf MSR-TR | pdf FM2014]
• It’s Alive! Continuous Feedback in UI Programming.
  Sebastian Burkhart, Manuel Fahndrich, Peli del Halleux, Sean McDirmid, Michał Moskal, Nikolai Tillmann, and Jun Kato. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2013)
  [pdf | video]
• The Future of Teaching Programming is on Mobile Devices.
  Nikolai Tillmann, Michał Moskal, Jonathan de Halleux, Manuel Fahndrich, Judith Bishop, Arjmand Samuel, and Tao Xie. 17th Annual Conference on Innovation and Technology in Computer Science Education (ITiCSE 2012) .
  [pdf]
• Search by Example in TouchDevelop: Code Search Made Easy
  Marat Akhin, Nikolai Tillmann, Manuel Fahndrich, Jonathan de Halleux, and Michał Moskal. 2012 ICSE Workshop on Search-Driven Development-Users, Infrastructure, Tools and Evaluation
• Engage Your Students by Teaching Programming Using Only Mobile Devices with TouchDevelop
  Nikolai Tillmann, Michał Moskal, Jonathan de Halleux, Manuel Fahndrich, and Tao Xie. 24th IEEE-CS Conference on Software Engineering Education and Training (CSEE&T 2012). Tutorial.
• Engage Your Students by Teaching Programming Using Only Mobile Devices with TouchDevelop (abstract only)
  Nikolai Tillmann, Michał Moskal, Jonathan de Halleux, Manuel Fahndrich, and Tao Xie. 43rd ACM Technical Symposium on Computer Science Education (SIGCSE 2012) Workshop summary.
• Verifying implementations of security protocols by refinement.
  Nadia Polikarpova, Michał Moskal. Verified Software: Theories, Tools and Experiments (VSTTE 2012).
  [pdf]
• TouchDevelop: Programming Cloud-Connected Mobile Devices via Touchscreen.
  Nikolai Tillmann, Michał Moskal, Jonathan de Halleux, Manuel Fähndrich. ONWARD '11 at SPLASH. Also MSR-TR-2011-49.
  [pdf]
• The Boogie Verification Debugger.
  Claire Le Goues, K. Rustan M. Leino, Michał Moskal. Software Engineering and Formal Methods (SEFM 2011). To appear.
  [pdf]
• Heaps and Data Structures: A Challenge for Automated Provers.
  Sascha Böhme, Michał Moskal. 23rd International Conference on Automated Deduction (CADE 2011).
  [pdf | pdf (new results) | web (benchmarks)]
• Verifying Concurrent C Programs with VCC.
  Ernie Cohen, Mark Hillebrand, Michał Moskal, Wolfram Schulte, Stephan Tobies. Working draft, version 0.2 The VCC tutorial, slightly updated for VCC3.
  [pdf 2-col. (~25 pp.) | pdf 1-col. (~65 pp.) | pdf screen (for reading directly on the screen)]
• Fat Pointers, Skinny Annotations: A Heap Model for Modular C Verification.
  Sascha Böhme, Michał Moskal. Draft. [The benchmark parts are superseded by Heaps and Data Structures: A Challenge for Automated Provers above, but the VCC3 memory model description is only present in this paper.]
  [pdf]
• Evidential Authorization.
  Andreas Blass, Yuri Gurevich, Michał Moskal, Itay Neeman. Bulletin of Euro. Assoc. for Theor. Computer Science 102, October 2010, to appear
  [pdf]
• The Unthinkable: Automated Theorem Provers for (Tracing) Just-in-time Compilers.
  Nikolai Tillmann, Michał Moskal, Wolfram Schulte, Herman Venter, Manuel Fahndrich. FIT: Fun Ideas and Thoughts session at PLDI 2010
  [pdf]
• VACID-0: Verification of Ample Correctness of Invariants of Data-structures, Edition 0.
  K. Rustan M. Leino, Michał Moskal. Tools & Experiments Workshop at VSTTE 2010 Supercool verification benchmarks! Try them with your tool, and submit solutions!
  [pdf]
• Local Verification of Global Invariants in Concurrent Programs.
  Ernie Cohen, Michał Moskal, Wolfram Schulte, Stephan Tobies. Computer Aided Verification (CAV 2010) (LNCS 6174). VCC methodology paper.
  [pdf]
• Satisfiability Modulo Software.
  Michał Moskal. PhD thesis. University of Wrocław. Submitted in September 2009, defended on December 1st, 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). (LNCS 5674). Wolfram's invited talk. The paper to cite for VCC.
  [pdf]
• Invariants, Modularity, and Rights.
  Ernie Cohen, Eyad Alkassar, Vladimir Boyarinov, Markus Dahlweid, Ulan Degenbaev, Mark A. Hillebrand, Bruno Langenstein, Dirk Leinenbach, Michał Moskal, Steven Obua, Wolfgang J. Paul, Hristo Pentchev, Elena Petrova, Thomas Santen, Norbert Schirmer, Sabine Schmaltz, Wolfram Schulte, Andrey Shadrin, Stephan Tobies, Alexandra Tsyban, Sergey Tverdyshev. Perspectives of Systems Informatics, 7th International Andrei Ershov Memorial Conference, PSI 2009. (LNCS 5947). Notes on VCC philosophy, largely by Ernie Cohen.
  [pdf]
• Deductive Verification of System Software in the VerisoftXT Project.
  Bernhard Beckert, Michał Moskal. Künstliche Intelligenz. Vol. 24, no. 1, April 2010. Springer.
  [pdf]
• Programming with Triggers.
  Michał Moskal. SMT '09: Proceedings of the 7th International Workshop on Satisfiability Modulo Theories. ACM International Conference Proceeding Series; Vol. 375, pages 20-29. Montreal, 2009. An updated version (compared to SMT2009), 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, Vol. 44(1-2), pp. 111-144..
  [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]

old talks

• TouchDevelop: a mobile IDE in the cloud
  Invited talk at PEPM 2014 workshop, in place of Manuel Fahndrich. For a more recent take on the ideas presented take a look at the Beyond Open Source paper below.
  [pptx]
  TouchDevelop: cross-platform app creation on mobile devices
  Tutorial at PLDI 2013.
  [pptx]
• TouchDevelop: A touch-first IDE for the Web created with TypeScript
  At //BUILD/2012 developer conference, November 1 2012.
  [recording]
• From C to infinity and back: Unbounded auto-active verification with VCC
  At CAV 2012, July 9 2012.
  [HTML (page with examples and instructions)]
• Verifying Functional Correctness C Programs with VCC.
  At NASA Formal Methods 2011, April 19 2011.