=========
Description
=========
Hybrid systems are complex dynamical systems that combine discrete and continuous components. Reachability questions, regarding whether a system can run into a certain subset of its state space, stand at the core of verification and synthesis problems for hybrid systems. Successful reachability analysis methods for hybrid systems require the unification of techniques from at least two research areas:

)) Symbolic methods that operate on exact and discrete representations of systems, in the form of various model checking and theorem proving algorithms.
)) Numerical methods that operate on various forms of numerical approximations and continuous transformations of the systems, as developed in the area of continuous dynamical systems and control theory.

The existing, successful solutions for reachability analysis for hybrid dynamical systems cleverly integrate symbolic and numerical reasoning to tackle the scalability challenge. For instance, the reachable set computation methods explicitly construct flow-pipes that numerically overapproximate the reachable states over time, while efficient computation of such overapproximations requires symbolic representations such as support functions. Similarly, constraint solving methods symbolically encode reachability properties as logic formulas, while solving such formulas requires numerically-driven decision procedures. The key goal of the Symbolic and Numerical Methods for Reachability Analysis (SNR) workshop is to provide a platform to further explore synergies among these approaches by bringing together the experts in these two domains.

=====
Scope
=====
The SNR workshop aims to catalyze work on the interface of symbolic and numerical methods for the reachability analysis. The scope of the workshop includes, but is not restricted to, the following topics:

** Verification of hybrid systems
** Symbolic representation of regions in reachability analysis
** Techniques for Flow-pipe construction
** Abstraction techniques for hybrid systems and numerical programs
** Trajectory/Counterexample generation from symbolic paths
** Techniques for reliable integration
** Decision procedures supporting real numbers
** Formal logics to reason about hybrid systems
** Symbolic and Numerical Methods for Reinforcement Learning and Planning
** Domain specific approaches in Biology, Robotics, and Cyber-Physical Systems

This year, the organizers encourage submissions of papers exploring the intersection of SNR and Machine-Learning (ML). Machine Learning (ML) algorithms and data-driven components are at the core of modern engineering applications of hybrid dynamical systems providing support for perception and adaptation. Moreover, the recent successes of Deep Neural Networks (DNN) and Reinforcement Learning (RL) hint at powerful approaches to tackle scalability challenges in SNR. We invite research papers at the intersection of SNR and ML on the following non-exhaustive list of topics:

** Reinforcement Learning (RL) for Real-Time and Hybrid Systems,
** Formal Logics for Continuous-State RL (e.g., formal specifications in RL, shielding for RL),
** Decision Procedures for Continuous-State RL (e.g. SAT/SMT approaches to infer reward machines),
** Deep Neural networks for Symbolic and Numerical Reasoning for Reachability (e.g., neural certificates),
** Supervised Learning for SNR (e.g., using decision-trees in generating human-interpretable policies),
** Unsupervised Learning for SNR (e.g., mining formal specifications from behaviors), and
** Applications of SNR in safety-critical machine learning.

The topic of the workshop has direct connections with the conferences within the CONFEST (e.g., FORMATS and CONCUR) and we believe that participants of the main conference may be interested in attending SNR and vice-versa. The workshop format is intended to complement the main conference by providing an informal meeting place specifically for researchers involved in the projects requiring the background both in symbolic and numerical verification.

================
Submission Information
================

The workshop solicits

** long research papers (not exceeding 15 pages excluding references),
** short research papers (not exceeding 6 pages excluding references) and
** work-in-progress papers (not exceeding 6 pages excluding references).

Research papers must present original unpublished work which is not submitted elsewhere. In order to foster the exchange of ideas, we also encourage work-in-progress papers, which present recent or on-going work. The papers should be written in English and formatted according to the EPTCS guidelines. Papers can be submitted using the EasyChair system. All submissions will undergo a peer-reviewing process.

Accepted research papers will be presented at the workshop and will be published in the Electronic Proceedings in Theoretical Computer Science (EPTCS). Accepted work-in-progress papers will be presented at the workshop but will not be included in the proceedings.