SNR 2020

Given the COVID-19 situation, SNR’20 will be conducted virtually. The main event announced small, but non-zero registration fees (5€ for a registration that covers all workshops of the event).

The 6th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR) will take place in Vienna, Austria as a satellite event of QONFEST'20.

Scope

The workshop on Symbolic-Numeric methods for Reasoning about CPS and IoT (SNR) focuses on the combination of symbolic and numeric methods for reasoning about Cyber-Physical Systems and the Internet of Things to facilitate model identification, specification, verification, and control synthesis problems for these systems. The synergy between symbolic and numerical approaches is fruitful for two main reasons:

  • Symbolic methods that operate on exact and discrete representations of systems, the set of reachable states, the distribution of model parameters or the possible gains for controller parameters.
  • Numeric 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.
Such synergies are already seen in areas such as reachability analysis (symbolic representation of reachable states versus numerical integration), uncertainty reasoning (eg., Rao-Blackwellization), machine learning (eg., learning models through stochastic gradient descent versus symbolic reasoning over the function represented by the network to prove properties) and decision procedures (eg., symbolic SAT solvers versus numerical convex optimization solvers).

Topics

The SNR workshop aims to catalyze work on the interface of symbolic and numeric methods for verification, synthesis and identification problems for CPS and IoT. The scope of the workshop includes, but is not restricted to, the following topics:

  • Verification, parameter identification and control synthesis for hybrid systems
  • Probabilistic inference and reachability for stochastic hybrid systems
  • Symbolic and numerical integration and decision techniques
  • Emerging applications to safe autonomous systems in uncertain environments
  • Resiliency and dependability in CPS and IoT

We encourage submissions of papers in the following two specific areas:
  • Verification of models used in machine learning and autonomous CPS
    Learning algorithms are at the core of many engineering applications including robotics and autonomous vehicles. We invite research papers on verification of models used in machine learning and autonomous CPS. In particular, recent advances in autonomous cars require addressing challenging questions around their safety and reliability.
  • Symbolic and numerical techniques for verification and synthesis of stochastic models
    Autonomous systems operate in uncertain environments. Thus, it is essential to reason about the effect of uncertainty. We invite research papers on symbolic and numerical techniques for formal synthesis of stochastic systems.

Invited talks

  • Invited Industrial Talk: Hermann Schichl, DAGOPT, University of Vienna
  • TBA
  • Invited Tutorial: Alberto Griggio, Fondazione Bruno Kessler:
    Solving non-linear arithmetic with SAT modulo theories and abstraction
    This tutorial will provide an introduction to SAT and SAT modulo theories solving techniques and their applications to deciding the satisfiability of formulae involving non-linear arithmetic. We will discuss how we can leverage the power of the symbolic search engines combined with abstraction and refinement to develop a simple, yet effective procedure for non-linear polynomial constraints over the reals. We will then show how the procedure naturally extends to handle also integer constraints and some common transcendental functions, and how it can be easily integrated into state-of-the-art symbolic verification engines for infinite-state transition systems.

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 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.

Call for Papers

TXT PDF

Important Dates

Camera-ready version August 20, 2020
Workshop August 31, 2020

Committee

Program Committee:
Thao Dang (co-chair, Verimag/CNRS, France)
Stefan Ratschan (co-chair, Academy of Sciences of the Czech Republic)
Naijun Zhan (Institute of Software, Chinese Academy of Sciences)
Sergiy Bogomolov (Newcastle University, United Kingdom)
Taylor T. Johnson (Vanderbilt University, U.S.A.)
Martin Fränzle (Carl von Ossietzky Universität Oldenburg, Germany)
Indranil Saha (Indian Institute of Technology Kanpur)
Milan Češka (Brno University of Technology, Czech Republic)
Goran Frehse (ENSTA Paris, France)
Sofie Haesaert (Eindhoven University of Technology, The Netherlands)
Jens Oehlerking (Robert Bosch GmbH, Germany)
Erika Ábrahám (RWTH Aachen University, Germany)

Steering Committee:

Program

Invited talks

Contributed Talks:

  • Andreas Rauh and Julia Kersten: Verification and Reachability Analysis of Fractional-Order Differential Equations Using Interval Analysis
  • Negin Musavi, Dawei Sun, Sayan Mitra, Geir Dullerud and Sanjay Shakkottai: Optimistic Optimization for Statistical Model Checking with Regret Bounds
  • Auguste Bourgois and Luc Jaulin: Interval centered form for proving stability of nonlinear discrete-time system
  • Tommaso Dreossi, Giorgio Ballardin, Parth Gupta, Jan Bakus, Yu-Hsiang Lin and Vamsi Salaka: Analysis of E-commerce Ranking Signals via Signal Temporal Logic

Solicited Talks:

Previous Workshops

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