I am a PhD student at the Department of Computer Science at the University of York. My research interests are in the area of formal methods and software verification, particularly with the formalisms Z, CSP and Circus.
My current research is on verification of virtual machines for Safety-Critical Java (SCJ). SCJ is a variant of Java designed to facilitate the creation of certifiable real-time systems. There has been work on verification of SCJ programs in the hiJaC project and its areas of application include robotics, making it a good implementation language for the ongoing RoboCalc project. I am working on modelling of an SCJ virtual machine in the Circus specification language and and verification of a compilation strategy from Java bytecode to C to permit native execution of SCJ programs.
Email: jeb531 [at] york.ac.uk
Phone: +44 (0)1904 325437