Extending EVA to 16 and 32 Bit Systems


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.

Fields of Study

  • 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

Hints for Applications

Please take a look at the Hints for applications.


This website uses cookies. By using the website, you agree with storing cookies on your computer. If you do not agree please leave the website.More information about cookies

RWTH Aachen University - Chair of Computer Science 11 - Ahornstr. 55 - 52074 Aachen - Germany