VORTEX 2025 – Verification and Monitoring at Runtime Execution
8th Workshop on Verification and Monitoring at Runtime Execution
Runtime Monitoring (RM) is concerned with the runtime analysis of software and hardware system executions in order to infer properties relating to system behaviour. Example applications include telemetry, log aggregation, threshold alerting, performance monitoring and adherence to correctness properties (more commonly referred to as runtime verification). RM has gained popularity as a solution to ensure software reliability, bridging the gap between formal verification and testing: on the one hand, the notion of event trace abstracts over system executions, thus favoring system agnosticism to better support reuse and interoperability; on the other hand, monitoring a system offers more opportunities for addressing error recovery, self-adaptation, and issues that go beyond software reliability. The goal of VORTEX is to bring together researchers contributing on all aspects of RM covering and possibly integrating both theoretical and practical aspects, with particular focus on hybrid approaches inspired by formal methods, program analysis, testing, and artificial intelligence.
The organization of this workshop was partially funded by the MUR project “T-LADIES” (PRIN 2020TL3X8X)
Keynote
Fri 4 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:15 | |||
09:00 15mDay opening | Opening VORTEX | ||
09:15 30mTalk | Runtime Monitoring of Action Specifications for Replanning in Classical Planning VORTEX File Attached | ||
09:45 30mTalk | Bounded Compositional Runtime Enforcement VORTEX Saumya Shankar , Srinivas Pinisetty Indian Institute of Technology Bhubaneswar, Thierry Jéron INRIA, Prisha Srinidi Indian Institute of Technology Bhubaneswar File Attached | ||
10:45 - 12:30 | |||
10:45 30mTalk | Aggregate Monitoring of Spatial Formulas beyond SLCS VORTEX Giorgio Audrito Università di Torino, Gianluca Aguzzi Alma Mater Studiorum - Università di Bologna, Mirko Viroli Alma Mater Studiorum - Università di Bologna File Attached | ||
11:15 30mTalk | Bounded Time Monitoring in Aggregate Systems VORTEX Giorgio Audrito Università di Torino, Ferruccio Damiani University of Turin, Gianluca Torta Dipartimento di Informatica - Università di Torino, Italy File Attached | ||
11:45 30mTalk | Monitors for distributed deadlock detection VORTEX Radosław Jan Rowicki Technical University of Denmark, Adrian Francalanza University of Malta, Alceste Scalas Technical University of Denmark File Attached | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:45 | |||
14:00 60mKeynote | Tell Me The Future, Correctly: On The Monitorability of Timed Logics Over Infinite Executions VORTEX | ||
15:00 30mTalk | Ain’t No Stopping Us Monitoring Now (extended abstract) VORTEX Luca Ciccone University of Turin, Francesco Dagnino , Angelo Ferrando University of Modena and Reggio Emilia File Attached | ||
Talks
Call for Papers
Submissions are expected to be in English and to belong to one of the following two categories:
- long paper, page limit 12 in
jotstyle: unpublished self-contained work - short paper, page limit 6 in
jotstyle: original contribution, not yet fully developed
Authors of submissions that clearly fall within the topics of interest will be invited to present their work at the workshop.
Topics of interest include, but are not limited to, the following ones:
- monitor construction and synthesis techniques
- program adaptation
- monitoring oriented programming
- runtime enforcement, fault detection, recovery and repair
- combination of static and dynamic analyses
- specification formalisms for RM
- specification mining
- monitoring concurrent/distributed systems
- RM for safety and security
- RM for the Internet of Things
- industrial applications
- integrating RM, formal verification, testing, and artificial intelligence
- tool development
- instrumentation techniques for RM
- surveys on different RM tools, formal frameworks or methodologies
- presentations of RM tools
- techniques for enhancing code coverage in offline RM
Papers must be submitted electronically via EasyChair; the submission deadlines are April 25th AoE (abstract) and May 2nd AoE (paper). Authors should use the jot style.
Remark: Attendance should be in person, on line presentations at the workshop will be supported only in case of compelling circumstances.
Proceedings: see the specific page
Proceedings and special issue
Authors of selected papers will be invited to contribute with extended versions to be included in a special issue of the Journal of Object Technology - JOT.
More recent VORTEX publications
| Fri 4 Jul 2025 Workshop |
| Wed 28 May 2025 Early registration deadline |
| Fri 16 May 2025 Author notification |
| Sun 4 May 2025 Paper submission deadline (extended) |
Davide AnconaCo-chair
DIBRIS, University of Genova, Italy
Italy
Giorgio AudritoCo-chair
Università di Torino
Italy
Antonis Achilleos
Reykjavik University
Diana Carolina Benjumea Hernandez
The University of Manchester, UK
United Kingdom
Silvia Bonfanti
University of Bergamo
Italy
Daniela Briola
University of Milano Bicocca
Italy
Einar Broch Johnsen
University of Oslo
Norway
Michele Chiari
TU Wien
Austria
Christian Colombo
University of Malta
Malta
João F. Ferreira
INESC-ID and IST, University of Lisbon
Portugal
Angelo Ferrando
University of Modena and Reggio Emilia
Italy
Carla Ferreira
NOVA University Lisbon
Portugal
Hannah Gommerstadt
Vassar College
Sung-Shik Jongmans
University of Groningen
Netherlands
Doron Peled
Bar Ilan University
Israel
Srinivas Pinisetty
Indian Institute of Technology Bhubaneswar
Kristin Yvonne Rozier
Iowa State University
Alceste Scalas
Technical University of Denmark
Denmark
Gerardo Schneider
University of Gothenburg
Sweden
Gianluca Torta
Dipartimento di Informatica - Università di Torino, Italy