A machine model describes the semantics of a particular processor family, including the instruction set, processor state, etc. When reasoning at the level of assembly language, for example in compilation or proof-carrying code, the machine model is at the core of any proof of correctness; if the model is flawed, then the entire system is potentially unsound.

Currently, these models are generated manually from the hardware reference manual, and as such may contain errors. A tool that checks that the machine model matches the hardware it represents would give more confidence in the model. Ideally, a model would be verified against the implementation, i.e. the physical hardware. Unfortunately, this is non-trivial: a naive approach would require checking each of a huge number of system states. Therefore, this thesis will look at validating the machine model, i.e. checking some subset of the possible states and providing an argument that the results obtained make sense.

A good thesis would involve:

• Investigating existing literature on model checking and formal machine models;
• Producing (or adapting) a machine model;
• Designing and writing a tool for checking the model against the hardware;
• Evaluating the tool and method;

The tool produced would, for example, simulate an instruction in the formal model, execute the instruction on the processor, and compare the results. Also, the tool should be easily configurable to different machine models and, ideally, different architectures.

Warning: this is an open ended problem. It will also require a student who is able to deal with both formal systems and low-level systems programming.