AVeRTS: Algorithmic Verification of Real-Time Systems

About AVeRTS

The aim of AVeRTS workshop is to provide a forum for researchers interested in the development of formal methods and algorithmic techniques for the analysis of probabilistic and real-time systems, and their application in automated verification of complex software and hardware systems. The satisfaction of time critical properties are crucial for ensuring safety in a wide range of computer science domains. The modeling, and the verification of such systems are hence of utmost importance. Algorithmic verification is an effective approach to analyse many properties of real-time systems: estimation of worst-case execution time, verification of timed specifications, synthesis of timely controllers, task scheduling and planning, etc. While these problems arise from different communities, formal methods provide a uniform approach to reason about timing constraints on the behaviors of systems. Several formalisms have been studied to model real-time systems (e.g. timed automata, timed Petri nets, etc) and formalize their specifications (e.g. metric temporal logic, timed computation tree logic, etc). In the recent years, stochastic models and logics have been introduced for quantitative evaluation of real-time systems, e.g. timeliness, reliability, response time, etc. The broad scope of the workshop includes

• [Foundations and semantics:] theoretical aspects of timed and probabilistic systems, languages and comparison between different models such as timed automata, timed Petri nets, hybrid automata, probabilistic models, timed logics;
• [Methods and tools:] algorithms, data structures, and software tools for analyzing timed and probabilistic systems with a focus on optimization and model-checking; The range of performance metrics of interest in probabilistic systems spans classical measures involving performance and reliability, as well as quantification of properties that are classically qualitative, such as safety, correctness, and security.
• [Applications:] case studies highlighting the role of quantitative evaluation in the design of systems, where the notion of system is broad. Systems of interest include computer hardware and software architectures, communication systems, embedded systems, infrastructural systems, and biological systems. Moreover, tools for supporting the practical application of research results in all of the above areas are of special interest.