Welcome to the MIPS-Why3k Development

The MIPS 32-bit architecture is used worldwide in teaching Computer Engineering due to its clean and simple design. This project aims to extend on the traditional view of the Hardware/Software interface to include aspects of modelling, code verification, code analysis, and certified programming.

To this end we undertake the approach of deductive program verification as provided by the Why3 platform.

The development is ongoing (started September 2015), in parallel with teaching Micro-Computer Engineering (D0013E) at Luleå University of Technology (LTU). Hence the material will be subject to continuous updates and changes. The documentation roughly follows the presented material during classes as follows:

Planned content (currently not implemented/demonstrated)