Student research opportunities
A Formal Semantics for a micro VM
Project Code: CECS_967
This project is available at the following levels:
Honours, Summer Scholar, Masters, PhD
Keywords:
theory,formal methods,virtual machine
Supervisors:
Dr Michael NorrishProfessor Steve Blackburn
Outline:
This project is to develop a formal (mathematical) description of aspects of the micro Virtual Machine that is being developed in the Computer Systems group. The virtual machine will soon have at least one prototype implementation, but we also want to describe its functionality mathematically.
This will have two benefits:
- Implementors of the virtual machine will have a solid specification of exactly what they must do
- Important functional properties of implementations may be verifiable. For example, type safety: stating that it is impossible for a well-behaved machine to have a type error when it executes.
Goals of this project
Depending on the research background of the student, and the time-scale, we will choose an aspect of the virtual machine to specify (examples would include: the dynamic behaviour of the bytecode instructions, the static type system, and the VM’s concurrency primitives). We would specify this sub-system in logic (almost certainly using the HOL4 theorem-proving system), and then
- prove whatever theorems about the system were appropriate; and/or
- demonstrate that the specification could be implemented (naïvely, perhaps) by programming in SML, or even HOL4’s own “functional language”.
