At our institute the model checker [mc]square for embedded software is developed. At the time being it supports the microcontrollers Atmel ATmega16 und ATmega128, Intel 8051, Infineon XC167, and Renesas R8C/23. Furthermore programmable logic controllers and abstract state machines are supported.

[mc]square creates the state space of the program under consideration by symbolically executing it in a simulator. In order to keep the state space managable [mc]square implements several abstraction techniques. One promissing technque is the Extended Value Annotation (EVA) that supports byte-wise nondeterminism.

The current implementation of EVA limits the application to 8 bit systems, because on of the symbolic annotation grows exponentially in the word size. This annotation has to be improved such that EVA can be used with 16 and 32 bit systems.

The [mc]square Team consists of 15 members in Aachen and at other universities. We offer an open-minded, helpful working atmosphere, modern workstations, and a fully automatic coffee dispenser.

• Computer science
• Electrical Engineering

Helpful, but not required skills are:

• Programming experiance in Java
• Experiance using Eclipse
• Lecture model checking
• Experiance with microcontrollers
• Proficiencies in German and English

Please take a look at the Hints for applications.

• Dr.rer.nat. Bastian Schlich