Welcome to the home page of the 8th International Workshop on Symbolic-Numeric Methods for reachability Analysis (SNR). SNR'22 will collocate with CONFEST'22 in Warsaw, Poland, on September, 12th 2022.

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.

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 \item 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).

SNR and Machine Learning.

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.

Organizers

Previous Workshops

• 7th Int. Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR’21), affiliated with QONFEST'21.
• 6th Int. Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR’20), affiliated with QONFEST'20.
• 5th Int. Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR’19), affiliated with CPS-IoT Week 2019.
• 4rd Int. Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR’18), affiliated with ETAPS'18.
• 3rd Int. Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR’17), affiliated with ETAPS'17.
• 2nd Int. Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR’16), affiliated with CPSWeek’16
• 1st Int. Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR’15), affiliated with CAV’15