I am a research associate 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 developing a formal testing strategy for robot software as part of the RoboTest project, on which I began work as a research associate in July 2018. This is part of the wider RoboStar group of projects and focusses on model-based test case development using the graphical specification notation RoboChart. I am working on extending the semantics of RoboChart to distinguish inputs and outputs, and using that information to extract timed test cases.
I completed my PhD at the University of York in January 2019, with a thesis entitled Ahead-of-time Algebraic Compilation for Safety-Critical Java, supervised by Ana Cavalcanti. My PhD research looked at verification of virtual machines for Safety-Critical Java (SCJ), a variant of Java designed to facilitate the creation of certifiable real-time systems. I worked 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: james.baxter [at] york.ac.uk
Phone: +44 (0)1904 325437