The VASSAL (Verification and Analysis for Safety and Security of Applications in Life) Workshop is a dedicated forum organized within the Runtime Verification 2025 conference taking place in Graz, Austria. The forum will bring together researchers from the EU Twinning funded VASSAL project and the broader runtime verification community. The VASSAL project is a collaboration between Brno University of Technology (Czechia), CEA-List (France), and TU Wien (Austria), with associated partner Honeywell (Czechia). The project focuses on advancing the safety, security, and resilience of software systems by integrating model-based design, formal methods, and runtime verification techniques. The workshop objective is to showcase the project’s recent scientific contributions and encourage discussions on emerging issues and research directions in safety of verification and analysis.
The workshop program will feature invited talks from leading experts, presentations from VASSAL researchers, and selected contributions from the runtime verification community. Topics of interest include runtime monitoring, automated synthesis, decision procedures, specification and verification of hyperproperties, dynamic analysis for concurrency, and AI-driven verification techniques.
The goal of the VASSAL Workshop is to promote communication and interaction between the formal methods and runtime verification communities, encourage teamwork in research, and investigate the practical application of verification technologies in industrial sectors like aerospace and automotive. The workshop will offer a friendly, open environment for exchanging ideas and discovering potential collaborations.
Webpage of the project: https://vassal.fit.vut.cz
The VASSAL project seeks to enhance software safety and security by integrating model-based design with formal verification techniques for automated system analysis. The project’s focus spans multiple key areas:
By addressing these challenges, VASSAL aims to improve the reliability, security, and resilience of critical systems, particularly in automotive, aerospace, and other safety-critical applications.
Runtime Verification (RV) has established itself as a mature and practical approach to reasoning about system correctness during execution. Striking a careful balance between formal rigor and real-world applicability, RV has become a reliable companion in the quest for safe and predictable systems. Yet, RV encompasses much more than its original role.
In this talk, I will open the RV box to reveal the many hidden diamonds within. Beyond its traditional role in correctness monitoring, RV unveils itself as one of the most multifaceted and versatile techniques in the systems engineering toolbox. We will explore how the same foundational mechanisms that enable real-time system monitoring can be adapted and employed to mine specifications, guide test generation, steer control decisions safely, and even localize and explain faults. This presentation invites you to view Runtime Verification not just as a tool for detecting property violations, but as a dynamic framework for understanding, designing, and trusting complex systems.
Dr. Nickovic is a leading expert in runtime verification and cyber-physical systems, with a deep research focus on monitoring temporal properties, contract-based design, and real-time systems. He is perhaps best known as a co-author of the influential paper “Monitoring Temporal Properties of Continuous Signals”, which introduced Signal Temporal Logic (STL) — a widely adopted specification formalism for reasoning about real-valued signals in dynamic systems. The paper has had a significant impact on the field, garnering over 1600 citations to date.
Beyond his foundational research, Dr. Nickovic has actively collaborated with numerous experts in the community, in particular with our TU Wien VASSAL Project partner Ezio Bartocci, further contributing to the advancement of monitoring, falsification analysis, mining formal specifications, and contract-based design in safety-critical and embedded systems.
With a rich academic journey that includes a Ph.D. under the guidance of Oded Maler at VERIMAG (Université Joseph Fourier), and postdoctoral research with Tom Henzinger at IST Austria, Dr. Nickovic brings a wealth of knowledge and experience to our workshop.
Dynamic logic (DL) is a mutli-modal logic, where modalities are parameterised over actions from some action language. The action language may be a programming language, or consist of (primitive or composed) steps of a system or component, or of environment moves. In this talk, I introduce principles of DL, and show how DL based verification can be practically used for effective verification on various levels of systems. Moreover, I discuss the relation of DL to other logics for verification.
Wolfgang Ahrendt is a professor at Chalmers University of Technology, Gothenburg, Sweden. He received his Ph.D. in Computer Science from the University of Karlsruhe, Germany, in 2001. His contributions lie in deductive verification of software, runtime verification, and combinations of static verification with runtime verification and testing. Wolfgang Ahrendt is one of the people behind the software verification approach and system ‘KeY’. Recent application areas of his work include automotive software safety, smart contracts, and AI assisted development of reliable software.
| 08:55-09:00 | Opening |
|---|---|
| 09:00-10:00 | Keynote 1 (Dejan Nickovic, A Box Full of Diamonds: The Many Facets of Runtime Verification) |
| 10:00-10:30 | Break |
| 10:30-12:10 | Session 1: Synthesis and SMT (5 x 20mins)
|
| 12:10-13:30 | Lunch Break |
| 13:30-13:45 | Presentation of the VASSAL project |
| 13:45-14:45 | Keynote 2 (Wolfgang Ahrendt, Dynamic Logic for Verification) |
| 14:45-15:15 | Coffee Break |
| 15:15-17:15 | Session 2: Requirements and program analysis (6 x 20mins)
|
We invite presentation abstracts (1-2 pages) describing ongoing research, recent results, concrete use cases, or works already published in international venues. At least one author of the accepted presentation is expected to present their work at the workshop at Graz, Austria.
We welcome submissions on all aspects of software verification, runtime analysis, and system safety, including but not limited to:
Contributions addressing challenges in safety-critical systems (automotive, aerospace, medical devices) are especially encouraged.
Presentation abstracts (1-2 pages) must be written in English and submitted electronically in PDF format using the link below. The 1-2 page limit includes all text and figures, but excludes references.
Abstracts will be evaluated by a Program Committee (PC) composed of VASSAL project leaders and members of the Runtime Verification community.
There will be no formal proceedings, but presentations will be listed on the workshop website.