Reachability analysis for annotated code. - Mikolás Janota; Radu Grigore; Michal Moskal (SAVCBS, 2007)

Edit and verify - Radu Grigore; Michal Moskal (CoRR, 2007)

E-matching for Fun and Profit. - Michal Moskal; Jakub Lopuszanski; Joseph R. Kiniry (SMT@CAV, 2007)

Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving. - Stefan Maus; Michal Moskal; Wolfram Schulte (AMAST, 2008)

Rocket-Fast Proof Checking for SMT Solvers. - Michal Moskal (TACAS, 2008)

Invariants, Modularity, and Rights. - Ernie Cohen; Eyad Alkassar; Vladimir Boyarinov; Markus Dahlweid; Ulan Degenbaev; Mark A. Hillebrand; Bruno Langenstein; Dirk Leinenbach; Michal Moskal; Steven Obua; Wolfgang J. Paul; Hristo Pentchev; et al. (Ershov Memorial Conference, 2009)

VCC: Contract-based modular verification of concurrent C. - Markus Dahlweid; Michal Moskal; Thomas Santen; Stephan Tobies; Wolfram Schulte (ICSE Companion, 2009)

VCC: A Practical System for Verifying Concurrent C. - Ernie Cohen; Markus Dahlweid; Mark A. Hillebrand; Dirk Leinenbach; Michal Moskal; Thomas Santen; Wolfram Schulte; Stephan Tobies (TPHOLs, 2009)

A Precise Yet Efficient Memory Model For C. - Ernie Cohen; Michal Moskal; Stephan Tobies; Wolfram Schulte (SSV, 2009)

Evidential Authorization. - Andreas Blass; Yuri Gurevich; Michal Moskal; Itay Neeman (The Future of Software Engineering, 2010)

Local Verification of Global Invariants in Concurrent Programs. - Ernie Cohen; Michal Moskal; Wolfram Schulte; Stephan Tobies (CAV, 2010)

HOL-Boogie - An Interactive Prover-Backend for the Verifying C Compiler. - Sascha Böhme; Michal Moskal; Wolfram Schulte; Burkhart Wolff (J. Autom. Reason., 2010)

Deductive Verification of System Software in the Verisoft XT Project. - Bernhard Beckert; Michal Moskal (Künstliche Intell., 2010)

Heaps and Data Structures: A Challenge for Automated Provers. - Sascha Böhme; Michal Moskal (CADE, 2011)

The role of information fusion in providing analytical rigor for intelligence analysis. - Michal Moskal; Moises Sudit; Kedar Sambhoos (FUSION, 2011)

Verifying Functional Correctness of C Programs with VCC. - Michal Moskal (NASA Formal Methods, 2011)

TouchDevelop: programming cloud-connected mobile devices via touchscreen. - Nikolai Tillmann; Michal Moskal; Jonathan de Halleux; Manuel Fähndrich (Onward!, 2011)

The Boogie Verification Debugger (Tool Paper). - Claire Le Goues; K. Rustan M. Leino; Michal Moskal (SEFM, 2011)

From C to Infinity and Back: Unbounded Auto-active Verification with VCC. - Michal Moskal (CAV, 2012)

Engage Your Students by Teaching Computer Science Using Only Mobile Devices with TouchDevelop. - Nikolai Tillmann; Michal Moskal; Jonathan de Halleux; Manuel Fähndrich; Tao Xie 001 (CSEE&T, 2012)

The future of teaching programming is on mobile devices. - Nikolai Tillmann; Michal Moskal; Jonathan de Halleux; Manuel Fähndrich; Judith Bishop; Arjmand Samuel; Tao Xie 001 (ITiCSE, 2012)

User-aware privacy control via extended static-information-flow analysis. - Xusheng Xiao; Nikolai Tillmann; Manuel Fähndrich; Jonathan de Halleux; Michal Moskal (ASE, 2012)

Engage your students by teaching programming using only mobile devices with TouchDevelop (abstract only). - Nikolai Tillmann; Michal Moskal; Jonathan de Halleux; Manuel Fähndrich; Tao Xie 001 (SIGCSE, 2012)

TouchDevelop: app development on mobile devices. - Nikolai Tillmann; Michal Moskal; Jonathan de Halleux; Manuel Fähndrich; Sebastian Burckhardt (SIGSOFT FSE, 2012)

Verifying Implementations of Security Protocols by Refinement. - Nadia Polikarpova; Michal Moskal (VSTTE, 2012)

It's alive! continuous feedback in UI programming. - Sebastian Burckhardt; Manuel Fähndrich; Peli de Halleux; Sean McDirmid; Michal Moskal; Nikolai Tillmann; Jun Kato 001 (PLDI, 2013)

Addressing JavaScript JIT Engines Performance Quirks: A Crowdsourced Adaptive Compiler. - Rafael Auler; Edson Borin; Peli de Halleux; Michal Moskal; Nikolai Tillmann (CC, 2014)

Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier. - K. Rustan M. Leino; Michal Moskal (FM, 2014)

Refactoring local to cloud data types for mobile apps. - Michael Hilton; Arpit Christi; Danny Dig; Michal Moskal; Sebastian Burckhardt; Nikolai Tillmann (MOBILESoft, 2014)

Exposing native device APIs to web apps. - Arno Puder; Nikolai Tillmann; Michal Moskal (MOBILESoft, 2014)

TouchDevelop: create rich mobile apps on touch devices (tutorial). - Nikolai Tillmann; Michal Moskal; Jonathan de Halleux; Sebastian Burckhardt; Thomas Ball 001; Judith Bishop (MOBILESoft, 2014)

Beyond Open Source: The Touch Develop Cloud-Based Integrated Development Environment. - Thomas Ball 001; Sebastian Burckhardt; Jonathan de Halleux; Michal Moskal; Jonathan Protzenko; Nikolai Tillmann (MOBILESoft, 2015)

Implementing real-time collaboration in TouchDevelop using AST merges. - Jonathan Protzenko; Sebastian Burckhardt; Michal Moskal; Jedidiah McClurg (MobileDeLi, 2015)

User-aware privacy control via extended static-information-flow analysis. - Xusheng Xiao; Nikolai Tillmann; Manuel Fähndrich; Jonathan de Halleux; Michal Moskal; Tao Xie 001 (Autom. Softw. Eng., 2015)

Microsoft touch develop and the BBC micro: bit. - Thomas Ball 001; Jonathan Protzenko; Judith Bishop; Michal Moskal; Jonathan de Halleux; Michael Braun; Steve Hodges 001; Clare Riley (ICSE (Companion Volume), 2016)

A System-General Model for the Detection of Gaming the System Behavior in CTAT and LearnSphere. - Luc Paquette; Ryan S. Baker 001; Michal Moskal (AIED (2), 2018)

MakerArcade: Using Gaming and Physical Computing for Playful Making, Learning, and Creativity. - Teddy Seyed; Peli de Halleux; Michal Moskal; James Devine; Joe Finney; Steve Hodges 001; Thomas Ball 001 (CHI Extended Abstracts, 2019)

Static TypeScript: an implementation of a static compiler for the TypeScript language. - Thomas Ball 001; Peli de Halleux; Michal Moskal (MPLR, 2019)

Microsoft MakeCode: embedded programming for education, in blocks and TypeScript. - Thomas Ball 001; Abhijith Chatra; Peli de Halleux; Steve Hodges 001; Michal Moskal; Jacqueline Russell (SPLASH-E, 2019)

MakeCode and CODAL: Intuitive and efficient embedded systems programming for education. - James Devine; Joe Finney; Peli de Halleux; Michal Moskal; Thomas Ball 001; Steve Hodges 001 (J. Syst. Archit., 2019)

The BBC micro: bit: from the U.K. to the world. - Jonny Austin; Howard Baker; Thomas Ball 001; James Devine; Joe Finney; Peli de Halleux; Steve Hodges 001; Michal Moskal; Gareth Stockdale (Commun. ACM, 2020)

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 001; Thomas Ball 001; Asta Roseway (CHI, 2021)

Web-based Programming for Low-cost Gaming Handhelds. - Michal Moskal; Thomas Ball 001; Abhijith Chatra; James Devine; Peli de Halleux; Steve Hodges 001; Shannon Kao; Richard Knoll; Galen Nickel; Jacqueline Russell; Joey Wunderlich; Daryl Zuniga (FDG, 2021)

ML Blocks: A Block-Based, Graphical User Interface for Creating TinyML Models. - Randi Williams; Michal Moskal; Peli de Halleux (VL/HCC, 2022)

Plug-and-play Physical Computing with Jacdac. - James Devine; Michal Moskal; Peli de Halleux; Thomas Ball 001; Steve Hodges 001; Gabriele D'Amone; David Gakure; Joe Finney; Lorraine Underwood; Kobi Hartley; Paul Kos; Matt Oppenheim (Proc. ACM Interact. Mob. Wearable Ubiquitous Technol., 2022)

Meet MicroCode: a Live and Portable Programming Tool for the BBC micro: bit. - Kobi Hartley; Elisa Rubegni; Lorraine Underwood; Joe Finney; Thomas Ball 001; Steve Hodges 001; Peli de Halleux; James Devine; Eric Anderson; Michal Moskal (IDC, 2024)

Jacdac: Service-Based Prototyping of Embedded Systems. - Thomas Ball 001; Peli de Halleux; James Devine; Steve Hodges 001; Michal Moskal (Proc. ACM Program. Lang., 2024)

Plug-and-Play Physical Computing and Device Prototyping with Jacdac. - James Devine; Steve Hodges 001; Thomas Ball 001; Michal Moskal; Peli de Halleux; Gabriele D'Amone; David Gakure; Joe Finney; Lorraine Underwood; Kobi Hartley; Matt Oppenheim; Paul Kos (GetMobile Mob. Comput. Commun., 2024)

Generating Structured Outputs from Language Models: Benchmark and Studies. - Saibo Geng; Hudson Cooper; Michal Moskal; Samuel Jenkins; Julian Berman; Nathan Ranchin; Robert West 001; Eric Horvitz; Harsha Nori (CoRR, 2025)