About Me
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 focuses on model-based test case development using the graphical specification notation RoboChart. During this, I have extended the semantics of RoboChart to distinguish inputs and outputs, and developed a strategy to extract timed test cases. I am currently working to develop a language called RoboWorld to describe the environment of a robot. My current focus is defining the semantics of RoboWorld using a hybrid variant of Circus called CyPhyCircus, and working to apply hybrid model checkers to allow checking of the semantics.
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