This talk addresses model checking of microcontroller programs. Preliminary to the actual talk a short overview over model checking and microcontrollers is given. The talk starts with a motivation for model checking microcontroller source code. It is described why assembly code instead of C code was chosen for model checking. After that, the model checking tool [mc]square is detailed. The features are itemized, the procedure used is presented, and several details of the architecture are depicted. Next, some features used during model checking are explained in detail (e.g. handling of nondeterminism). Subsequently, two programs are introduced which are used in the following live presentation of the tool. In the end a conclusion is drawn and some potentials for future improvements are described.