1st workshop on STAtic + Runtime verification Synergies
23 November 2026 – Satellite event of SEFM 2026, Malta
STARS 2026 is new a forum for researchers interested in exploring and advancing the integration of static and runtime verification techniques.
The registration to STARS 2026 is now open through the SEFM 2026 registration page. The early registration deadline is 23 October.
Programme
Here is the list of talks that will be presented at STARS 2026. The detailed workshop schedule will be announced soon.
- Invited Talk: A Retrospective on Trace Expressions: The Past, the Present and the Future
- Invited Talk: Verifying a Blockchain Node's Network Behaviour using Typestate + Session Types in Rust
- Invited Talk: Static and Runtime Verification on Multiparty Session Protocols
- Runtime Verification under Uncertainty: Experiences from STARK
- Towards Low-Latency Model-Based Trace-Checking in Maude
- Dynamic Device Environments in Runtime Verification: Monitoring Power Consumption in Smart Homes
- Experimental Safety Verification of Autoware through Simulink Modeling and SMT-Based Analysis
- Distributed Monitoring of Multiparty Session Protocols using Relative Types
- Verifying Fault Tolerance using Multiparty Session Types
Invited Talk: A Retrospective on Trace Expressions: The Past, the Present and the Future
Trace expressions are a formal, system-agnostic language tailored for rewriting-based runtime verification, specifically designed to bridge the gap between rigorous formal methods and the practical needs of software engineers. In this talk, I will first introduce the core formalism and outline its operational semantics, built on the foundational notion of Antimirov's partial derivatives. Next, I will showcase how the formalism is employed in significant real-world applications. Finally, I will discuss open challenges and directions for future research, including the relationship between trace expressions and behavioral types.
Short Bio
Davide Ancona is an Associate Professor at the University of Genoa, Italy. He is a senior investigator and coordinator for the "Secure and Reliable Systems" research line within the DIBRIS department. His main research interests include Runtime Verification, type systems, and the design and foundations of programming languages. He is currently the President of the Executive Board of AITO, which serves as the steering committee for ECOOP. Since 2016, he has been co-organizing the VORTEX workshop on Runtime Verification, co-located with ECOOP.
Invited Talk: Verifying a Blockchain Node's Network Behaviour using Typestate + Session Types in Rust
This talk presents the ongoing work towards the correct-by-construction implementation of Amaru, a new Cardano blockchain node client written in Rust. One of the most challenging aspects of this work is the correct implementation of the proof-of-stake protocol used in Cardano, called Ouroboros; this challenge is further complicated by the fact that Amaru is a concurrent program based on actors, which are notoriously difficult to verify. This talk will illustrate the main iterations of our design and implementation of Amaru: in particular, how we modelled the Ouroboros protocol specification using a variant of session types, and how we enforced this specification in Amaru's Rust code (with different approaches, including runtime monitoring and compile-time type-level computations) to ensure that Amaru's internal actors never deadlock and implement Ouroboros correctly.
Short Bio
Roland Kuhn works on Cardano node diversity, including consensus and deterministic simulation for Amaru, and consults on satellite operations and distributed systems. He is the author of Reactive Design Patterns and co-author of the Reactive Manifesto. Previously, he was CTO and co-founder of Actyx and led the Akka project at Lightbend.
Invited Talk: Static and Runtime Verification on Multiparty Session Protocols
Multiparty session types (MPST) provide a principled approach to specifying and verifying concurrent and distributed systems, ensuring safety, deadlock-freedom, and liveness of communicating agents and programs. In this talk, I will present recent advances in static, runtime, and hybrid verification based on MPST. I will discuss the relationship between correctness-by-design and model-checking approaches (POPL'25, OOPSLA'26, ESOP'27), refinement-based hybrid verification in Rust (ECOOP'24), asynchronous communication optimisations (TOCL'24, TOCL'26, Inf. Comp.'26), and recent applications of Large Language Models (LLMs) (ASE'26).
Short Bio
Nobuko Yoshida is Christopher Strachey Chair of Computer Science at the University of Oxford. She is an EPSRC Established Career Fellow and an Honorary Fellow at Glasgow University. Over the last 10 years, her main research interests have been theories and applications of protocol specifications and verification. She introduced multiparty session types [POPL08, JACM], which received the Most Influential POPL Paper Award in 2018 (judged by its influence over the last decade). This work enlarged the community and widened the scope of applications of session types, e.g. runtime monitoring based on Scribble (co-developed with Red Hat) has been deployed to other projects such as cyberinfrastructure in the US Ocean Observatories Initiative (OOI), and widened the scope of her research areas. She received the Test-of-time-award from PPDP'24 and the best paper awards from CC'20, COORDINATION'23, DisCoTech'23 and ECOOP'23. She received the third Suffrage Science Awards for Mathematics and Computing from MRC for her STEM activity. She is an editorial board member of ACM Transactions on Programming Languages and Systems, Theoretical Computer Science, ACM Formal Aspects of Computing, Journal of Logical Algebraic Methods in Programming, Actor Informatica and the chief editor of The Computer-aided Verification and Concurrency Column for EATCS Bulletin.
Runtime Verification under Uncertainty: Experiences from STARK
The STARK tool set has been introduced for the verification and analysis of systems operating under uncertainty. It offers evolution sequences for the representation of system behaviour, namely sequences of distributions over states generated by a model of a program operating in an evolving environment.
We have been working on runtime verification (RV) of systems under uncertainty using STARK. Since the evolution-sequence model was originally developed for (static) statistical model checking, we have adapted our framework to support runtime observations.
This presentation explains the challenges encountered in developing a formal theory of RV in this context, as well as the lessons learned from developing a safety shield for an autonomous-driving case study.
Towards Low-Latency Model-Based Trace-Checking in Maude
Modern software engineering embraces practices such as unit testing and continuous integration, while formal verification techniques remain largely confined to specialized domains. However, as software systems become increasingly distributed, complex, and safety-critical, stronger validation mechanisms become ever more necessary. Achieving wider adoption of formal validation requires approaches that are accessible to everyday developers and aligned with existing workflows.
We present Linoleum, an application for checking properties over OpenTelemetry traces using Maude specifications. By operating directly on real execution traces, Linoleum remains close to the mental models developers already use for debugging and monitoring. It employs the OpenTelemetry ecosystem to facilitate adoption in production environments and supports continuous runtime validation of deployed systems. Linoleum scales horizontally using Apache Flink to spawn multiple distributed Maude interpreters, while properties are specified through lightweight Maude monitors. We demonstrate the usefulness of the approach with a chatbot case study and evaluate its scalability.
Dynamic Device Environments in Runtime Verification: Monitoring Power Consumption in Smart Homes
Runtime verification aims to determine satisfactions or violations of specifications by observing the current execution of a system. Recent advances within the field have focused more and more on monitoring multiple traces and determining the satisfaction of collective properties between them. Such a setup is that of smart homes, where smart appliances can be instrumented, controlled, and given pre-defined instructions via smart home managements systems. This digital shift has lead to an increased need for monitoring the power consumption behavior over time. Runtime Verification is well-suited for such specifications which often resemble standard temporal logic formalisms combined with basic arithmetic between numerical values. However, in current formal verification works, once a monitor has been synthesized and instrumented on a multiple component system, new components cannot be added at runtime, making the overall system quite static. Moreover, and once a verdict has been reached, the monitor must be restarted.
In this paper we address both of this issues. The static device environment is addressed- by defining a specification language called Power Metric Integer Interval Temporal Logic, which combines elements from temporal logics, dealing with temporal behavior, hyperlogics, dealing with multiple components, and stream based specifications, dealing with sensor inputs and basic arithmetic. The multiple verdicts issue is addressed by our monitoring synthesis for the safety fragment of our logic, for which we also provide a tool implementation and evaluation.
Experimental Safety Verification of Autoware through Simulink Modeling and SMT-Based Analysis
Formal verification can provide strong guarantees for mathematical models of autonomous driving systems, while the applicability of such guarantees to their actual software and hardware implementations remains a critical issue. In this work, we investigate a combined approach that connects static verification of a Simulink model with trajectory-based conformance checking of Autoware.
We first construct a Simulink model of main components of the Autoware control system, including Pure Pursuit-based lateral control, PID-based longitudinal control, and vehicle dynamics represented by a kinematic bicycle model. We can also use built-in blocks provided by the Automated Driving Toolbox to leverage industry expertise. The safety properties of this model are then analyzed using a dedicated model checker based on an SMT solver, providing static guarantees over the modeled behavior. The properties to be verified include the error relative to the target waypoints and the reachability of branch conditions in the model. To relate the verification results to Autoware, we execute corresponding driving scenarios in both Autoware and Simulink and compare their resulting trajectories. Autoware execution logs, including planned trajectories, vehicle poses, and velocities, are used to reproduce the scenarios in Simulink, and the conformance between the two systems is quantitatively evaluated using metrics such as the Skorokhod distance. It is based on a comparison of the states of the two systems across space and time.
This combination of static model checking and runtime conformance analysis provides a practical bridge between formal guarantees obtained for models developped with Simulink and the behavior of a complex autonomous driving implementation. Our experiments explore the potential of such a static and runtime synergy for increasing confidence in the safety of Autoware.
Distributed Monitoring of Multiparty Session Protocols using Relative Types
This talk proposal concerns a framework for the distributed monitoring of asynchronous, message-passing communication between components.
As protocol specifications, we consider global types from theories of Multiparty Session Types; as implementations, we consider components whose exact specification is unknown, with observable behavior but with minimal assumptions on their structure (“gray boxes”).
Leveraging recently-developed techniques based on relative types, we use global types to synthesize monitors for gray boxes, thereby unlocking the analysis of protocols not supported by prior works.
We formally define correctness for monitored components, and establish associated meta-theoretical results: we prove that monitored gray boxes are sound (they correctly follow the protocol) and transparent (gray boxes with and without monitors are behaviorally equivalent).
[Work based on results presented at RV'23 and soon to appear in the STTT journal.]
Verifying Fault Tolerance using Multiparty Session Types
Multiparty Session Types (MPST) are a behavioural type system for verifying communication-centric properties for multi-agent message-passing systems. They have seen much development over the past decade, including rich extensions for distributed systems under various network assumptions. But, can this rich ecosystem be used to verify more than just communication properties? This work-in-progress explores the use of MPST for verifying fault tolerance. We conjecture that some results can be achieved to this end through a combination of static and runtime verification. For the former, by developing theories of observational equivalence for both process and type semantics, and establishing connections between the two. For the latter, by using the session types to generate monitors that provide additional guarantees on the functional correctness of redundant components in the system.