Augusto Sampaio holds a DPhil from the University of Oxford, is a Doctor Honoris Causa of the University of York, a Commander of the Brazilian Order of Scientific Merit, a member of the Brazilian Academy of Sciences, and a Professor at the Universidade Federal de Pernambuco, Brazil. His main research interests include formal methods in software engineering; formal approaches to testing; the use of generative AI to automate the generation of formal specifications and to improve formal verification; the design, simulation, and verification of robotic systems; and the safe evolution of smart contracts in blockchains. He is a member of the Editorial Boards of Formal Aspects of Computing (ACM) and Science of Computer Programming (Elsevier). He has published more than 150 papers and supervised over 60 PhD and master’s students.

Peter Gorm Larsen is professor at the department of electrical and computer engineering in the section for Software Engineering & Computer Systems at Aarhus University in Denmark. He currently leads the AU Centre for Digitalisation, Big Data, and Data Analytics (DIGIT) and the AU Centre for Digital Twins. After receiving his M.Sc. in Electronic Engineering at the Technical University of Denmark in 1988, he worked in industry before returning to complete an industrial Ph.D. in 1995. In his industry career, as a development engineer and manager, he gave industrial courses all over the world on formal methods, and saw the technology he developed be applied in areas as diverse as secure message processing over options trading to near-field communication firmware. He returned to academia in 2005. His prime research goal now is to improve the development of complex mission-critical applications by implementing and applying well-founded technologies, in particular in the design of robust tools that help engineers to leverage models in early design stages to reduce overall product development risk in particular in the area of Cyber- Physical Systems and Digital Twins. Right now he is the overall coordinator of the Horizon Europe project called RoboSAPIENS.

Thierry Lecomte has 30 years of experience in R&D, having worked on industrial projects in the automotive, healthcare, microelectronics, nuclear energy, railway and space industries. Today he is R&D director of CLEARSY, a French SME specialized in the invention of safety critical systems, where he has worked since its creation in 2001. His current subjects of interest are safety and security co-engineering, safe artificial intelligence, and autonomous mobility - all related to formal methods.

Burkhart Wolff is a professor at the University Paris-Saclay and member of the “Laboratoire des Methodes Fomelles” (LMF). His main research interests focus on test- and proof based verification techniques and their semantic foundation in Isabelle/HOL. He is a major contributor to the Isabelle Archive of Formal Proofs (AFP) in general and CSP-related theories and proof techniques in particular. Currently, he is working on a process-algebraic approach to specify and reason over safe driving strategies in the autonomous vehicle domain.

I am a PhD student at the University of Bremen and an industry practitioner specializing in the intersection of software testing, verification, and safety-critical systems. My work focuses on making rigorous quality assurance an enabler for trustworthy innovation in high-assurance domains like avionics and railway systems. Key areas include: scenario-based testing of distributed, dynamically reconfigurable systems-of-systems; property-oriented module testing and temporal logic; model learning for symbolic and finite-state machines; testing methodologies for certification and safety standards. Parallel to my PhD, I apply formal methods and verification tools to industrial codebases. My work involves designing verification activities for aerospace and railway customers, developing simulation software, and ensuring compliance with stringent safety requirements. I also contribute to the company's strategic development in the field of business & technical interface and recruitment. I aim to bridge the gap between academic rigor and industrial practice. My goal is to develop scalable testing techniques that lower the barriers to formal methods, fostering a culture where safety and correctness are integral to the engineering process.

David A. Anisi received the Doctor- and Licentiate of Science degree in Optimization and Systems Theory and Master of Science degree in Engineering Physics, all from the Royal Institute of Technology (KTH) in Stockholm, Sweden. After more than a decade of industrial R&D experience at ABB in Oslo, Norway, within design, control and verification of intelligent robotic- and autonomous systems, he is now back in academia working as Associate Professor at University of Agder, as well as Robotics Group at the Norwegian University of Life Sciences (NMBU) where he also served as the Director of Master of Applied Robotics Program.

Radu Calinescu is Professor of Computer Science at the University of York, UK, where he leads a research team developing theory and tools for the modelling, verification, synthesis, and assurance of self-adaptive, autonomous, and AI systems. A central focus of his recent work is the operationalisation of normative requirements for autonomous agents. He has published over 200 research papers in the areas of software engineering, formal methods, and probabilistic modelling. He has served as a Program Co-Chair for international conferences including ICECCS, SEFM, SEAMS, ICSA, and ICPE, and is an Associate Editor for ACM Computing Surveys and ACM Transactions on Autonomous and Adaptive Systems.

Ana Cavalcanti is a Professor at the University of York, UK, and holds a Royal Academy of Engineering Chair in Emerging Technologies. In that role, she is Director of RoboStar. She previously held a Royal Society Industry Fellowship, which provided her with the ideal opportunity to understand and contribute to the practice of formal methods working with QinetiQ. Her main scientific achievements have been on the design and justification of sound refinement-based program development and verification techniques. She has covered theoretical and practical integration with industry-strength technology: concurrency, object-orientation, and testing, dealing now with mobile and autonomous robots. Her work provides support for graphical notations popular with engineers, and for main-stream programming languages. It is distinctive in that it has comprehensive coverage of practical languages, rather than idealised notations. It also supports high degrees of automation to enable usability and scalability. In York, she leads the Design and Verification pillar of the Institute for Safe Autonomy.

Jim Woodcock is a Professor of Software Engineering whose research focuses on formal methods: mathematical techniques for specifying, reasoning about, and verifying software and cyber-physical systems. His work spans programming semantics (including Unifying Theories of Programming), mechanised proof (notably with Isabelle/HOL), and the verification of safety-critical and AI-enabled systems. He collaborates internationally across academia and industry, with particular interests in rigorous assurance for autonomous and interconnected systems. He also contributes to the community through editorial and service roles, supporting high-quality research in formal specification and verification.

Simon Foster is a Senior Lecturer (Associate Professor) at the University of York, and member of the RoboStar Centre of Excellence on Software Engineering for Robotics. His primary research applies theorem proving to formal verification and he leads the development of Isabelle/UTP, a practical theorem prover for heterogeneous systems. He has applied Isabelle/UTP to verification tools for autonomous and mobile robots, cyber-physical systems, process algebras, and reactive programs. He has also developed Isabelle/SACM, an interactive tool for assurance cases with evidence coming from multiple formal verification tools in Isabelle. He teaches logic and formal proof to undergraduate students, and assured software engineering to industrialists.

Alvaro Miyazawa is a lecturer in the Department of Computer Science at the University of York and a member of the RoboStar Centre for Software Engineering for Robotics. He earned a BSc in computer science from the University of São Paulo and completed his doctoral research at the University of York. His primary research interests include formal semantics and refinement for domain-specific languages and graphical notations, as well as the development of verification strategies to enhance automation in program verification. Alvaro has applied and developed formal techniques across various fields, including systems engineering, safety-critical real-time systems, and robotics. Currently, his research focuses on modelling, testing, simulation, and verification in robotics.

Pedro Ribeiro is a Lecturer (Assistant Professor) in Computer Science at the University of York, UK. Previously, he was a Research Fellow in the School of Physics, Engineering and Technology at York, and before that, a Research Associate in Computer Science. He completed his PhD degree at York on the treatment of angelic nondeterminism for process calculi. He has over a decade of experience with formal approaches to software engineering relevant to robotics and cyber-physical systems more generally. His research interests span the breadth of the engineering lifecycle, spanning from design and development of domain-specific notations and their semantics, to testing and formal reasoning using automated mathematical proof techniques. He is a member of the York's RoboStar Centre for Excellence in Software Engineering for Robotics, and a founding member of Formal Methods Europe's communications committee. He received a best paper (SoSyM) award in 2019 for work on RoboChart. In 2025 he was awarded a grant on Large Language Models for lattice-theoretic reasoning of reactive programs by Renaissance Philanthropy as part of its AI for Math Fund.

I am a research associate working for the EU project RoboSapiens, and I am interested in engineering reliable robotic software involving AI components. My research involves combining multiple tools and techniques to enable automated reasoning on models of AI-enabled software. Practically, this involves adding support for modelling AI components in RoboChart, defining the formal semantics of these AI components, and then working on a verification approach for the complete (AI-enabled) RoboChart model using a combination of Isabelle and AI-specific verification tools, such as Marabou.

James Baxter is a researcher in the RoboStar centre 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. He has previously worked on the RoboTest project, developing a verified model-based testing strategy for robotic systems and the RoboWorld notation for capturing environment assumptions. He is now part of the RoboSAPIENS EU project, applying RoboStar notations and techniques to the development of self-adaptive robots.

Holly Hendry recently submitted her doctoral thesis on Human-Robot Interaction in the Design and Verification of Robotic Systems at the University of York, UK. Holly was a finalist at STEM for BRITAIN for her PhD research. She previously worked as a software engineer at Amazon, working with customers across a range of products. Currently, her work as a Research Associate at the University of York is experimenting with the potential use of AI in formal verification.