Keynotes

Elvira Albert, Complutense University of Madrid, Spain

Securely Optimized (Ethereum) Smart Contracts using Formal Methods

We will overview the application of various types of formal methods to optimize smart contracts and prove the correctness of the optimization results. Smart contracts are computer programs stored on a blockchain that are intended to automatically execute, control or document events and actions according to the terms of a contract or an agreement. The blockchain is one of the contexts in which the use of formal methods to enhance its security and efficiency is critical. On one hand, software bugs on smart contracts have already caused several high profile attacks and there is hence huge interest and investment in guaranteeing their correctness. Efficiency is of similar relevance as well, as deploying and executing smart contracts has a cost (in the corresponding cryptocurrency). Hence, optimization tools for smart contracts have been emerging since the last few years. The talk will present our work on optimizing the efficiency of Ethereum smart contracts and ensuring the correctness of the optimization results. The basis of our work is the use of formal methods, including SAT and SMT solvers, proof-assistants, rule-based transformations, static analyses and greedy algorithms. Finally, we will also discuss the use of machine learning technology to boost the efficiency of our formal methods-based techniques.

Robert M. Hierons, University of Sheffield, United Kingdom

Systematic testing for robotic systems

Robotic systems form the basis for advances in areas such as manufacturing, healthcare, and transport. A number of areas in which robotic systems are being used are safety-critical and so there is a need for software development processes that lead to robotic systems that are safe, reliable and trusted. Testing will inevitably be an important component.

This talk will describe recent work on automated testing of robotic systems. The work is model-based: it takes as input a state-based model that describes the required behaviour of the system under test. Models are written in either RoboChart, a state-based language for robotics, or RoboSim, a simulation language for robotics. These languages have been given a formal semantics, making it possible to reason about models in a sound manner. This talk will describe how the development of robotic software can be formalised based on such languages and how this can lead to the potential to automate the generation of sound test cases. Such test cases can be used for testing within a simulation and possibly also for testing the deployed system. Testing is systematic since test cases target potential faults.

Ricardo Pérez del Castillo, University of Castilla-La Mancha, Spain

Quantum Software in Action: Challenges and Opportunities in Software Engineering

Quantum computing is rapidly evolving from a theoretical promise to a practical reality, with profound implications for software engineering. As quantum hardware advances, the demand for rigorous methods, tools, and practices to design, verify, and maintain quantum software becomes increasingly critical. This talk examines the emerging field of quantum software engineering, with particular emphasis on the role of formal methods in ensuring correctness, reliability, and trustworthiness of quantum programs and hybrid quantum–classical systems. Key topics include quantum programming models, specification and verification techniques, testing approaches, scalability, and the integration of quantum algorithms into real-world applications. The talk also outlines opportunities for innovation in methodologies, frameworks, and interdisciplinary collaboration, providing a comprehensive perspective on how quantum software can transition from research prototypes to dependable systems.