2017 - current
Software Engineer
Apple Inc.

Leading and developing certification tools for HomeKit accessories

2015 - 2017
Software Engineer
Apple Operations Europe

Developing, arcitechturing and running several applications supporting Apples ecosystem certification programs.

2014 - 2015
Software Engineer (JavaScript)
Apozy Inc.

Working as a full-stack JavaScript developer, with a Node.js, MongoDB and Redis based backend, and with AngularJS, Bootstrap and HTML5 based front-end. In addition, I am responsible for web-ops processes like automatic deploy, server provisioning and cofiguration using Salt.

2013 - 2014
Software Systems Engineer/Team Lead
LitePoint Inc.

I led the developement of a software project that aided RF-engineers with data analyzis and vizualizations. The tool was build around a JavaScript platform with a stand-alone front-end, a data-sharing backend, and an auto pdf-report generating tool. Leading the project involved planning realeases that has to fullfil requirements from both internal engineering departments and external customers. Project stability was achieved using dedicated QA-engineers

2010 - 2013
Ph.D fellow
Aalborg University - Department of Computer Science

I was a Ph.D. fellow in the Embedded and Distributed Systems group. In my Ph.D., I am making formal verification more applicable in modern software development processes. Many of the existing formalisms are not expressive enough to model modern software systems. I am working towards extending this expressiveness while preserving the possibility of using the models for model checking. My main focus is on systems developed in software product lines and on systems based on asynchronously communicating components. My thesis is based on publications [0-4], and can be found on github.com/mikaelhm/phd.

2011 - present
Founder (Web Consultant/System admin)
Mikael Harkjær Møller

I am running my own small web-consultancy bureau. The majority of the projects have revolved around customized Wordpress-based websites. However, I am also developing more involved and custom solutions, like a monitoring system for a holiday house and a heating control system for a minor factory.

2011 - present
Co-Founder (System Administrator)
Urhost

Urhost is a small web-hosting company that I founded with a phd-colleague. Urhost specializes in dedicated Typo3 and Wordpress solutions.

2007 - 2010
Web-developer (student-job)
Sanistål A/S

I worked as a student developer on a web-shop front-end for a major Danish wholesale company. The front-end was implemented using XHTML, CSS, JavaScript, and PHP.

Degrees

Aalborg University - 2013
Ph.D. Degree from Computer Science and Engineering

Aalborg University - 2010
Master of Science in Computer Science (Cum Laude)

Aalborg University - 2008
Bachelor of Science in Computer Science and Mathematics

Skills

Programming Languages
Swift, Objective-C, Ruby, JavaScript, JSON, Yaml, Bash

Mastered Technologies/Frameworks
Ruby on Rails, HAML, Node.js, Chef, JSON, XML, MySQL, Nginx, Git, Web Services, Docker, LaTeX

Contact
How to get a hold of me

Address
700 Chiquita Ave, Apt. 3, Mountain View, 94041, California, USA

Phone
+1 669-600-9361

Mail
m@mikael.hm

GitHub
https://github.com/mikaelhm

Twitter
https://twitter.com/mhmoeller

LinkedIn
https://linkedin.com/in/mikaelhm/

Software Projects

Apozy - Gamified Security Awareness Training
Apozy is a training platform which aims at training employees of larger corps about security in a more fun and engaging maner. In addition, Apozy provides metrics to the company security managament about the employees knowledge, actions and additude towards security. The product is developed on a JavaScript-based stack, with Node.js as the backend-engine using the Sails.js platform (Ruby on Rails inspired) with no-SQL databases MongoDB and Redis. The front end is based on a AngularJS and Bootstrap, utilzing open source libraries like D3.js and GSAP, and more. The product is developed with a small team of 3 developers using agile process with code-reviews and short and fast release cycles. Approved change are automatically deployed a development environment for testing, and releases are automatically deployed on prodcution servers.

IQramp (LitePoint) - Data Analytics tool for RF-engineers
IQramp is a data analytics tool used by RF-engineers to get a better understading of test results, and easier debug and track down error in wireless communication. The product is developed on a JavaScript-based stack, initially with a Node.js and MongoDB backend and an AngularJS front-end. Later on, the product evolved into a stand-alone desktop tool, inorder to support in-factory engineers with no internet access. This was achived ising the node-webkit to shell the web-app and browserify let us reuse our Node.js modules, and implement the computational task of the backend in HTML5 WebWorkers. Data-sharing between RF-engineers was supported by a much simplified node.js backend developed using Synth.js

Vindstød - Web-service Client
I developed a communication module for a private Danish electricity supplier. The module integrates their existing management software with the national DataHub, a web-service for communication between players on the Danish electricity market. The module is implemented in Python and utilizes a MySQL database as an interface between itself and the existing platform.

Holiday Home Energy Monitoring
The purpose of this system is to report the energy consumption in a holiday house. The owner of the house wishes to ensure that the guests have lowered the pool and room temperatures before departure. The system consists of three parts: a sensor unit in the house, a simple web-service for logging the data, and a web-application that shows and visualizes the data. The sensor unit is based on an Electric Imp (a small micro-controller based system) that measures electricity usage, room temperature, and water temperature in the pool. The unit reports to the web-service, which is written in PHP. The web-application is implemented with Bootstrap and jQuery. It requests data from the web-service.

TAPAAL - Model-Checker
During my scientific work, I have mainly been working with formal verification. To demonstrate some of the results, I have developed the model checking tool TAPAAL in collaboration with some colleagues. TAPAAL is a user-friendly model-checker with a graphical editor and simulator. The development started six years ago, and is still active. The tool is mainly implemented in Java, but some of the engines are done in C++. My contribution is mainly based on the results published in [7-10].

Publications

[0] Channel Properties of Asynchronously Composed Petri Nets
S. Haddad, R. Hennicker, and M. H. Møller
In Proceedings of the 34th International Conference on Application and Theory of Petri Nets and Concurrency (PN'13), LNCS vol. 7927, p. 369-388
We present a set of relevant communication properties of asynchronously communicating systems. We prove that it is possible to verify these properties and that it can be done in an efficient way.

[1] Specification of Asynchronous Component Systems with Modal I/O-Petri Nets
S. Haddad, R. Hennicker, and M. H. Møller
In Proceedings of the 8th International Symposium on Trustworthy Global Computing (TGC 2013)
We extend the results of [1] and present a framework and method that support the development of systems based on asynchronously communicating component. The framework ensures that the communication in the system meets certain requirements.

[2] Parametric Modal Transition Systems
N. Benes, J. Kretinsky, K.G. Larsen, M.H. Møller, and J. Srba
In Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11) LNCS vol. 6996, p. 275-289
In this paper, we extend a well-known modelling framework to make it more applicable in software development processes. For instance, we are able to express optional features by this extension. Furthermore, we prove that if the abstract model has a certain property, then all implementations (all combinations of features) will have the property.

[3] Dual-Priced Modal Transition Systems with Time Durations
N. Benes, J. Kretinsky, K.G. Larsen, M.H. Møller, and J. Srba
In Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'12), LNCS vol 7180, p. 122-137
We extend the model from [3] even further with time and cost quantities. This gives the developers of a system the possibility to reason about implementation cost and running cost of a final implementation of the system. This method can also verify if there exists a possible implementation within the budget.

[4] A Characterizing Logic for Boolean Modal Transition Systems
M. H. Møller, K. G. Larsen, and X Liu
In Proceedings of the 8th Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'12)
In this paper, we present an add-on to the formalism presented in [3]. It is a formal logic that can determine which combination of features that yield an implementation that satisfies certain safety requirements.

[5] Compositional verification of real-time systems using Ecdar
A. David, K. G. Larsen, A. Legay, M. H. Møller, U. Nyman, A. P. Ravn, A. Skou and Andrzej Wąsowski
In International Journal on Software Tools for Technology Transfer, vol.14, no. 6, p. 703-720. Springer-Verlag, Germany
We present a method on how to perform compositional model-checking with the tool Ecdar. In compositional model-checking, model-checking is done component-wise. This makes it possible to apply model-checking to larger and more complex system models.

[6] Undecidability of Coverability and Boundedness for Timed-Arc Petri Nets with Invariants
L. Jacobsen, M. Jacobsen, and M.H. Møller
In Proceedings of the 5th Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS’09), Dagstuhl, Germany, 2009.
We present two undecidability results, showing that two important properties of Petri nets cannot always be decided for a certain extension of timed-arc Petri nets.

[7] A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking
L. Jacobsen, M. Jacobsen, M.H. Møller, and J. Srba
In Proceedings of the 7th European Performance Engineering Workshop (EPEW'10), LNCS vol. 6342, p. 83-98'
We provide a framework that makes it easier to prove the correctness of translations between formal specification formalisms. We formulate a set of requirements for the translation. The translation is correct if each requirement is met. In most cases, the requirements are easier to prove than the correctness itself.

[8] Verification of Timed-Arc Petri Nets
L. Jacobsen, M. Jacobsen, M.H. Møller, and J. Srba
In Proceedings of the 37th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM`11), LNCS vol. 6543, p. 46-72'
We present a way to perform formal verification of timed-arc Petri nets using an existing state-of-the-art model-checking tool for another formalism. The timed-arc Petri nets are translated into timed automata by an efficient algorithm. The translation is shown to be correct by the method presented in [8].

[9] TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets
A. David, L. Jacobsen, M. Jacobsen, K.Y. Jørgensen, M.H. Møller, and J. Srba
In Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS`12), LNCS vol 7214, p. 492-497
The paper is a tool presentation of our model-checking tool TAPAAL. TAPAAL is an easy-to-use and time-efficient model checker that we have developed on the basis of our theoretical results.