James Baxter is a researcher at the University of York. His research interests are in the area of software engineering, particularly formal methods, having done his PhD on verified compilation for Safety-Critical Java. For the past four years, he has been working on the RoboTest project, developing a verified model-based testing strategy for robotic systems.
Gustavo Carvalho is a lecturer at Centro de Informática of the Universidade Federal de Pernambuco (UFPE), Brazil. His main research interest is on Software Engineering, with emphasis on tests and formal methods. He has authored about 30 peer-reviewed publications, besides reviewing papers for international conferences (FM, SEFM, ICTAC, TASE) and journals (SCP, SoSyM, IST, IEEE TSE). In 2021, he served as the chair of the Formal Methods Special Group at the Brazilian Computer Society.
Alvaro Miyazawa is a lecturer at the Department of Computer Science of the University of York. His main research interests are in formal semantics and refinement for domain-specific languages and graphical notations, and the development of verification strategies to support high levels of automation in program verification. He has applied and developed formal techniques in various fields, including systems engineering, safety-critical real-time systems, and robotics. Currently, his research focuses on modelling, testing, simulation and verification for robotics.
Pedro Ribeiro is a research fellow in the RoboStar group at the University of York. His research interests are in formal modelling and verification of systems encompassing a broad range of aspects such as data, concurrency, time, and priorities. His doctoral work addressed the treatment of angelic nondeterminism in process calculi at the core of an approach for verification of control software. Since then, he has worked on techniques of relevance to software engineering for robotics. This includes the development of timed semantics for reasoning about the behaviour of robotic controllers, and establishing soundness of automatically generated simulations. Currently, his research focuses on automatic test generation for simulation and deployment in robotics.
Matt Windsor is a research associate in the RoboStar group at the University of York. Matt is mainly interested in the use of automated formal methods to reason about concurrent and reactive systems, having done a PhD on automating separation-style concurrent program logics. Matt has worked with the Interface Reasoning for Interacting Systems (IRIS) programme on the automatic testing of compilers to detect implementation mistakes with regards to C11 concurrency. Matt now works on the UKRI Trustworthy Autonomous Systems (TAS) Verifiability Node, focusing on delivering a specification language (RoboCert) for properties of robotic systems, as well as software modelling for Node case studies.
