![](https://dblp1.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp1.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp1.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
default search action
Michal Moskal
Person information
- affiliation: Microsoft Research, Redmond, WA, USA
Refine list
![note](https://dblp1.uni-trier.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j8]Thomas Ball
, Peli de Halleux
, James Devine
, Steve Hodges
, Michal Moskal
:
Jacdac: Service-Based Prototyping of Embedded Systems. Proc. ACM Program. Lang. 8(PLDI): 692-715 (2024) - [j7]James Devine, Steve Hodges, Thomas Ball, Michal Moskal, Peli de Halleux, Gabriele D'Amone, David Gakure, Joe Finney, Lorraine Underwood, Kobi Hartley, Matt Oppenheim, Paul Kos:
Plug-and-Play Physical Computing and Device Prototyping with Jacdac. GetMobile Mob. Comput. Commun. 28(2): 38-43 (2024) - [c40]Kobi Hartley
, Elisa Rubegni
, Lorraine Underwood
, Joe Finney
, Thomas Ball
, Steve Hodges
, Peli de Halleux
, James Devine
, Eric Anderson
, Michal Moskal
:
Meet MicroCode: a Live and Portable Programming Tool for the BBC micro: bit. IDC 2024: 355-370 - 2022
- [j6]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:
Plug-and-play Physical Computing with Jacdac. Proc. ACM Interact. Mob. Wearable Ubiquitous Technol. 6(3): 110:1-110:30 (2022) - [c39]Randi Williams, Michal Moskal, Peli de Halleux:
ML Blocks: A Block-Based, Graphical User Interface for Creating TinyML Models. VL/HCC 2022: 1-5 - 2021
- [c38]Teddy Seyed, James Devine, Joe Finney, Michal Moskal
, Peli de Halleux, Steve Hodges, Thomas Ball, Asta Roseway:
Rethinking the Runway: Using Avant-Garde Fashion To Design a System for Wearables. CHI 2021: 45:1-45:15 - [c37]Michal Moskal
, Thomas Ball, Abhijith Chatra, James Devine, Peli de Halleux, Steve Hodges, Shannon Kao, Richard Knoll, Galen Nickel, Jacqueline Russell, Joey Wunderlich, Daryl Zuniga:
Web-based Programming for Low-cost Gaming Handhelds. FDG 2021: 38:1-38:12 - 2020
- [j5]Jonny Austin, Howard Baker, Thomas Ball, James Devine
, Joe Finney
, Peli de Halleux, Steve Hodges, Michal Moskal
, Gareth Stockdale:
The BBC micro: bit: from the U.K. to the world. Commun. ACM 63(3): 62-69 (2020)
2010 – 2019
- 2019
- [j4]James Devine
, Joe Finney
, Peli de Halleux, Michal Moskal
, Thomas Ball, Steve Hodges:
MakeCode and CODAL: Intuitive and efficient embedded systems programming for education. J. Syst. Archit. 98: 468-483 (2019) - [c36]Teddy Seyed, Peli de Halleux, Michal Moskal
, James Devine
, Joe Finney
, Steve Hodges, Thomas Ball:
MakerArcade: Using Gaming and Physical Computing for Playful Making, Learning, and Creativity. CHI Extended Abstracts 2019 - [c35]Thomas Ball, Peli de Halleux, Michal Moskal
:
Static TypeScript: an implementation of a static compiler for the TypeScript language. MPLR 2019: 105-116 - [c34]Thomas Ball, Abhijith Chatra, Peli de Halleux, Steve Hodges, Michal Moskal
, Jacqueline Russell:
Microsoft MakeCode: embedded programming for education, in blocks and TypeScript. SPLASH-E 2019: 7-12 - 2018
- [c33]Luc Paquette, Ryan S. Baker, Michal Moskal:
A System-General Model for the Detection of Gaming the System Behavior in CTAT and LearnSphere. AIED (2) 2018: 257-260 - [c32]James Devine
, Joe Finney
, Peli de Halleux, Michal Moskal
, Thomas Ball, Steve Hodges:
MakeCode and CODAL: intuitive and efficient embedded systems programming for education. LCTES 2018: 19-30 - 2016
- [c31]Thomas Ball, Jonathan Protzenko, Judith Bishop, Michal Moskal
, Jonathan de Halleux, Michael Braun, Steve Hodges, Clare Riley:
Microsoft touch develop and the BBC micro: bit. ICSE (Companion Volume) 2016: 637-640 - 2015
- [j3]Xusheng Xiao
, Nikolai Tillmann, Manuel Fähndrich, Jonathan de Halleux, Michal Moskal
, Tao Xie:
User-aware privacy control via extended static-information-flow analysis. Autom. Softw. Eng. 22(3): 333-366 (2015) - [c30]Thomas Ball, Sebastian Burckhardt, Jonathan de Halleux, Michal Moskal
, Jonathan Protzenko, Nikolai Tillmann:
Beyond Open Source: The Touch Develop Cloud-Based Integrated Development Environment. MOBILESoft 2015: 83-93 - [c29]Jonathan Protzenko, Sebastian Burckhardt, Michal Moskal
, Jedidiah McClurg:
Implementing real-time collaboration in TouchDevelop using AST merges. MobileDeLi 2015: 25-27 - 2014
- [c28]Rafael Auler, Edson Borin, Peli de Halleux, Michal Moskal, Nikolai Tillmann:
Addressing JavaScript JIT Engines Performance Quirks: A Crowdsourced Adaptive Compiler. CC 2014: 218-237 - [c27]K. Rustan M. Leino, Michal Moskal:
Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier. FM 2014: 382-398 - [c26]Nikolai Tillmann, Michal Moskal
, Jonathan de Halleux, Sebastian Burckhardt, Thomas Ball, Judith Bishop:
TouchDevelop: create rich mobile apps on touch devices (tutorial). MOBILESoft 2014: 1-2 - [c25]Arno Puder, Nikolai Tillmann, Michal Moskal
:
Exposing native device APIs to web apps. MOBILESoft 2014: 18-26 - [c24]Michael Hilton
, Arpit Christi, Danny Dig, Michal Moskal
, Sebastian Burckhardt, Nikolai Tillmann:
Refactoring local to cloud data types for mobile apps. MOBILESoft 2014: 83-92 - 2013
- [c23]Sebastian Burckhardt, Manuel Fähndrich, Peli de Halleux, Sean McDirmid, Michal Moskal
, Nikolai Tillmann, Jun Kato
:
It's alive! continuous feedback in UI programming. PLDI 2013: 95-104 - 2012
- [c22]Michal Moskal:
From C to Infinity and Back: Unbounded Auto-active Verification with VCC. CAV 2012: 6 - [c21]Nikolai Tillmann, Michal Moskal
, Jonathan de Halleux, Manuel Fähndrich, Tao Xie:
Engage Your Students by Teaching Computer Science Using Only Mobile Devices with TouchDevelop. CSEE&T 2012: 87-89 - [c20]Nikolai Tillmann, Michal Moskal
, Jonathan de Halleux, Manuel Fähndrich, Judith Bishop, Arjmand Samuel, Tao Xie:
The future of teaching programming is on mobile devices. ITiCSE 2012: 156-161 - [c19]Xusheng Xiao
, Nikolai Tillmann, Manuel Fähndrich, Jonathan de Halleux, Michal Moskal
:
User-aware privacy control via extended static-information-flow analysis. ASE 2012: 80-89 - [c18]Nikolai Tillmann, Michal Moskal
, Jonathan de Halleux, Manuel Fähndrich, Tao Xie:
Engage your students by teaching programming using only mobile devices with TouchDevelop (abstract only). SIGCSE 2012: 663 - [c17]Nikolai Tillmann, Michal Moskal
, Jonathan de Halleux, Manuel Fähndrich, Sebastian Burckhardt:
TouchDevelop: app development on mobile devices. SIGSOFT FSE 2012: 39 - [c16]Nadia Polikarpova, Michal Moskal:
Verifying Implementations of Security Protocols by Refinement. VSTTE 2012: 50-65 - 2011
- [c15]Sascha Böhme, Michal Moskal:
Heaps and Data Structures: A Challenge for Automated Provers. CADE 2011: 177-191 - [c14]Michal Moskal
, Moises Sudit, Kedar Sambhoos:
The role of information fusion in providing analytical rigor for intelligence analysis. FUSION 2011: 1-6 - [c13]Michal Moskal:
Verifying Functional Correctness of C Programs with VCC. NASA Formal Methods 2011: 56-57 - [c12]Nikolai Tillmann, Michal Moskal
, Jonathan de Halleux, Manuel Fähndrich:
TouchDevelop: programming cloud-connected mobile devices via touchscreen. Onward! 2011: 49-60 - [c11]Claire Le Goues
, K. Rustan M. Leino, Michal Moskal:
The Boogie Verification Debugger (Tool Paper). SEFM 2011: 407-414 - 2010
- [j2]Sascha Böhme, Michal Moskal
, Wolfram Schulte, Burkhart Wolff:
HOL-Boogie - An Interactive Prover-Backend for the Verifying C Compiler. J. Autom. Reason. 44(1-2): 111-144 (2010) - [j1]Bernhard Beckert, Michal Moskal
:
Deductive Verification of System Software in the Verisoft XT Project. Künstliche Intell. 24(1): 57-61 (2010) - [c10]Andreas Blass, Yuri Gurevich, Michal Moskal, Itay Neeman:
Evidential Authorization. The Future of Software Engineering 2010: 73-99 - [c9]Ernie Cohen, Michal Moskal, Wolfram Schulte, Stephan Tobies:
Local Verification of Global Invariants in Concurrent Programs. CAV 2010: 480-494
2000 – 2009
- 2009
- [c8]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, Elena Petrova, Thomas Santen, Norbert Schirmer, Sabine Schmaltz, Wolfram Schulte, Andrey Shadrin, Stephan Tobies, Alexandra Tsyban, Sergey Tverdyshev:
Invariants, Modularity, and Rights. Ershov Memorial Conference 2009: 43-55 - [c7]Markus Dahlweid, Michal Moskal
, Thomas Santen, Stephan Tobies, Wolfram Schulte:
VCC: Contract-based modular verification of concurrent C. ICSE Companion 2009: 429-430 - [c6]Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, Stephan Tobies:
VCC: A Practical System for Verifying Concurrent C. TPHOLs 2009: 23-42 - [c5]Ernie Cohen, Michal Moskal
, Stephan Tobies, Wolfram Schulte:
A Precise Yet Efficient Memory Model For C. SSV 2009: 85-103 - 2008
- [c4]Stefan Maus, Michal Moskal, Wolfram Schulte:
Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving. AMAST 2008: 284-298 - [c3]Michal Moskal:
Rocket-Fast Proof Checking for SMT Solvers. TACAS 2008: 486-500 - 2007
- [c2]Mikolás Janota
, Radu Grigore, Michal Moskal
:
Reachability analysis for annotated code. SAVCBS 2007: 23-30 - [c1]Michal Moskal
, Jakub Lopuszanski, Joseph R. Kiniry:
E-matching for Fun and Profit. SMT@CAV 2007: 19-35 - [i1]Radu Grigore, Michal Moskal:
Edit and verify. CoRR abs/0708.0713 (2007)
Coauthor Index
aka: Peli de Halleux
![](https://dblp1.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-16 19:29 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint