International Workshop on Verification and mOnitoring at Runtime EXecutionVORTEX 2021
VORTEX brings together researchers working on all aspects of Runtime Monitoring (RM) with emphasis on integration with formal verification and testing.
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.
Mon 12 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
10:30 - 11:50
|Increasing Confidence in Autonomous Systems
I: Michael Fisher University of Manchester, UKFile Attached
|Test’n’Mo: A Collaborative Platform for Human Testers and Intelligent Monitoring Agents
Filippo Ricca DIBRIS, University of Genova, Italy, Viviana Mascardi DIBRIS, University of Genova, Italy, Alessandro VerriFile Attached
|RVPLAN: A General Purpose Framework for Replanning using Runtime Verification
13:30 - 14:50
|The E-ACSL Perspective on Runtime Assertion Checking
Julien Signoles CEA LISTFile Attached
|Towards Aggregate Monitoring of Spatio-temporal Properties
|RM for Users’ Safety and Security in the Built Environment
Giorgio Audrito Università di Torino, Ferruccio Damiani University of Turin, Giuseppe Di Giuda , Silvia Meschini , Laura Pellegrini , Elena Seghezzi , Lavinia Chiara Tagliabue , Lorenzo Testa , Gianluca TortaFile Attached
15:30 - 16:50
|Synchronous and Asynchronous Stream Runtime Verification
I: César Sánchez IMDEA Software InstituteFile Attached
|Optional Monitoring for Long-Lived Transactions
|Runtime Verification for Trustworthy Secure Shell Deployment
Call for Papers
Submissions are expected to be in English and to belong to one of the following two categories:
- regular paper, page limit 8 in
acmartstyle: unpublished self-contained work
- extended abstract, page limit 4 in
acmartstyle: original contribution, not yet fully developed
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, and testing
- tool development
- instrumentation techniques for RM
- surveys on different RM tools, formal frameworks or methodologies
- presentations of RM tools
Papers must be submitted electronically via EasyChair; the submission deadline is April 30 AoE. Authors should use the official ACM Master article template, which can be obtained from the ACM Proceedings Template pages.
Latex users should use the
sigconf option, as well as
review to produce line numbers for easy reference by the reviewers, as indicated by the following command:
Accepted regular papers and extended abstracts will be included in the proceedings published in the ACM Digital Library.
After the workshop, VORTEX speakers will be invited to contribute to a special issue of The Journal of Object Technology (JOT) with an extended version of their presented work.