RV25

Keynotes at RV25 will be given by our invited speakers Thomas Henzinger, Nils Jansen, Ankush Desai, and Daniela Micucci.

Thomas Henzinger

IST Austria, Austria

Nils Jansen

Ruhr-University Bochum, Germany

Ankush Desai

Amazon Web Services, USA

Daniela Micucci

University of Milano – Bicocca, Italy

TBA
TBA
Building reliable and secure software requires a range of approaches to reason about systems correctness. Alongside industry-standard testing methods (such as unit and integration testing), AWS has adopted model checking, fuzzing, property-based testing, fault-injection testing, deterministic simulation, event-based simulation, and runtime validation of execution traces. Formal methods have been an important part of the development process – perhaps most importantly, formal specifications as oracles or monitors that provide the correct answers for many of AWS’s testing practices. Correctness testing and formal methods remain key areas of investment at AWS. In this talk, we will cover some of these tools and techniques that have had impact within AWS and the also open challenges that remains to be solved to further amplify the adoption of formal methods in practice.
In digital health and pervasive computing, recognizing Activities of Daily Living (ADL) through inertial signals presents both opportunities and challenges. Human Activity Recognition (HAR) plays a key role in enabling systems that can monitor human behavior, supporting assisted living, improving rehabilitation processes, and providing context-aware services in smart environments. Inertial sensors, such as accelerometers and gyroscopes, offer a non-invasive, cost-effective, and energy-efficient means to capture continuous data on human motion. However, transforming raw data into reliable and meaningful activity recognition is non-trivial, particularly in real-world, dynamic settings.
This keynote will explore various approaches to HAR, highlighting their respective strengths and limitations. Special attention will be given to ensuring accurate and reliable activity detection, especially in real-time applications.
The talk will highlight challenges related to data diversity, user variability, and the continuous adaptation of recognition models.
Tom Henzinger is professor at the Institute of Science and Technology Austria (ISTA), chair of the Austrian Council for Sciences, Technology, and Innovation (FORWIT), and member of the Scientific Council of the European Research Council (ERC). He holds a Dipl.-Ing. degree in Computer Science from Johannes Kepler University in Linz, Austria, an M.S. degree in Computer and Information Sciences from the University of Delaware, a Ph.D. degree in Computer Science from Stanford University (1991), and Dr.h.c. degrees from Fourier University in Grenoble, France, and from Masaryk University in Brno, Czech Republic. He was Assistant Professor of Computer Science at Cornell University, Professor of Electrical Engineering and Computer Sciences at the University of California, Berkeley, Director at the Max-Planck Institute for Computer Science in Saarbruecken, Germany, and Professor of Computer and Communication Sciences at EPFL in Lausanne, Switzerland. From 2009 until 2022, he was the founding president of ISTA in Klosterneuburg, Austria. His research focuses on the theory of software systems, especially models, algorithms, and tools for the design and verification of reliable software. His HyTech tool was the first model checker for mixed discrete-continuous systems. He is a member of the US National Academy of Sciences, the American Academy of Arts and Sciences, Academia Europaea, the German Academy of Sciences (Leopoldina), the Austrian Academy of Sciences, and a Foreign Member of the Royal Society. He is a Fellow of the AAAS, the ACM, the IEEE, and the EATCS. He received the Robin Milner Award of the Royal Society, the EATCS Award of the European Association for Theoretical Computer Science, the Wittgenstein Award of the Austrian Science Fund (FWF), and two Advanced Grants of the ERC.

Nils Jansen is a full professor at the Ruhr-University Bochum, Germany, and leads the chair of Artificial Intelligence and Formal Methods. The mission of his chair is to increase the trustworthiness of Artificial Intelligence (AI). Nils Jansen is also an associate professor at Radboud University, Nijmegen, The Netherlands. He was a research associate at the University of Texas at Austin and received his Ph.D. with distinction from RWTH Aachen University, Germany. His research is on intelligent decision-making under uncertainty, focusing on formal reasoning about the safety and dependability of artificial intelligence (AI). He holds several grants in academic and industrial settings, including an ERC starting grant titled Data-Driven Verification and Learning Under Uncertainty (DEUCE). 

Ankush Desai is a Principal Applied Scientist at Amazon Web Services (AWS), where he develops tools and techniques to help developers build reliable distributed services. His research focuses on making rigorous software engineering practices accessible to developers, integrating formal methods, fuzzing, systematic testing, and runtime monitoring across the development lifecycle from design through production.

As the creator and lead developer of the P programming framework, his work has been particularly impactful in ensuring the correctness of critical systems, including USB drivers in Windows and distributed services at AWS. He earned his PhD in Computer Science from UC Berkeley (2019), receiving the Sevin Rosen Funds Award for Innovation for his research’s practical impact. Before his doctoral studies, he spent over two years at Microsoft Research India, where he worked on formal verification of device drivers and distributed systems.

Daniela Micucci is Associate Professor and head of the Software Architecture Lab at the University of Milano – Bicocca. Her research focuses on software engineering, with particular interest in software architecture, software development, and quality. She is active in digital health, with a focus on both infrastructures for remote monitoring systems and the recognition of human activities from sensed data using machine learning and deep learning techniques. She is also actively working on improving software development practices and quality, focusing on the role of Large Language Models in software engineering tasks, and on the design of techniques for assessing the robustness of conversational systems. She has published more than 100 papers, including several papers that appeared in top journals and conferences, such as TSE, TAAS, Pervasive and Mobile Computing, ICSE, FSE, RV, and ICPC.