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.
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
- 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
- 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.
| Optimization problems in the power market - to verify or not to verify | |
| Energy production is a surprisingly complex problem with conflicting modeling paradigms. On the one hand, electricity is not storable, so the power network must be balanced at all times, on the other hand there are several technologies available to store energy - from small scale systems like batteries to huge pump storage water plants. The various primary energy sources like wind, sunlight, oil, coal, lignite, and water combined together with various legal regulations lead to unusual constraints and very complex non-linear optimization problems. Is it worthwhile to apply algorithms based on verified computing techniques like interval analysis, or are purely numerical heuristic approaches preferable? |
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
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:
- Erika Ábrahám (RWTH Aachen, Germany)
- Sergiy Bogomolov (Australian National University)
- Martin Fränzle (University of Oldenburg, Germany)
- Taylor T. Johnson (Vanderbilt University, USA)
- Ashish Tiwari (SRI International, USA)
Program
The workshop will take place online using the tool ZOOM with meeting ID 974 5864 2202. Registered participants received the necessary password in their QONFEST welcome e-mail (slightly hidden after the list of workshops).
time is always in CEST (i.e., the time zone of Vienna, and a large part of the European Union)
- 8:45 - 9:45: Session 1
- Invited talk 1: Alberto Griggio: Solving non-linear arithmetic with SAT modulo theories and abstraction
abstract
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. - 9:45 - 10:15: Break
- 10:15 - 12:30: Session 2
-
- 10:15-10:40: Contributed talk 1
- Andreas Rauh and Julia Kersten: Verification and Reachability Analysis of Fractional-Order Differential Equations Using Interval Analysis
abstract
Interval approaches for the reachability analysis of initial value problems for sets of classical ordinary differential equations have been investigated and implemented by many researchers during the last decades. However, there exist numerous applications in computational science and engineering, where continuous-time system dynamics cannot be described adequately by integer-order differential equations. Especially in cases in which long-term memory effects are observed, fractional-order system representations are promising to describe the dynamics, on the one hand, with sufficient accuracy and, on the other hand, to limit the number of required state variables and parameters to a reasonable amount. Real-life applications for such fractional-order models can, among others, be found in the field of electrochemistry, where methods for impedance spectroscopy are typically used to identify fractional-order models for the charging/discharging behavior of batteries or for the dynamic relation between voltage and current in fuel cell systems if operated in a non-stationary state. This paper aims at presenting an iterative method for reachability analysis of fractional-order systems that is based on an interval arithmetic extension of Mittag-Leffler functions. An illustrating example, inspired by a low-order model of battery systems concludes this contribution. - 10:40-11:05: Contributed talk 2
- Negin Musavi, Dawei Sun, Sayan Mitra, Geir Dullerud and Sanjay Shakkottai: Optimistic Optimization for Statistical Model Checking with Regret Bounds
abstract
We present an algorithm and a tool for statistical model checking (SMC) of continuous state space Markov chains initialized to a set of states. This model checking problem requires maximization of probabilities of sets of executions over all choices of initial states. We observe that it can be formulated as a multi-armed bandit problem, and therefore, can be solved using hierarchical optimistic optimization. We propose a new algorithm (HOO-MB) and provide a regret bound on its sample efficiency which relies on the smoothness and the near-optimality dimension of the objective function and the sampling batch size. The batch size parameter enables us to strike a balance in the sample efficiency and the memory usage of the algorithm. Our experiments based on the implemented tool HooVer suggest that the approach scales to realistic-sized problems and is often more sample-efficient compared to PlasmaLab. Specifically, it has distinct advantages in analyzing models with a sharp slope around their worst initial conditions. - 11:05-11:30: Contributed talk 3
-
Auguste Bourgois and Luc Jaulin: Interval centered form for proving stability of nonlinear discrete-time system
abstract
In this paper, we propose a new approach to deal with the stability of non-linear discrete-time systems. We first show that the interval centered form plays of fundamental role in this context and makes it possible to easily prove the asymptotic stability of a discrete system. Then, we illustrate the principle of the approach through theoretical examples. Finally, we provide two practical examples using our approach : proving the stability of a localization system and proving the stability of a cycle described by a robot. - 11:30-12:00: Solicited talk 1
- Luc Jaulin: Characterizing Sliding Surfaces of Cyber-Physical Systems
abstract
When implementing a non-continuous controller for a cyber-physical system, it may happen that the evolution function of the closed-loop system is not anymore piecewise continuous along the trajectory, mainly due to if statements inside the control algorithm. As a consequence, an unwanted chattering effect may occur. This behavior is often difficult to observe even in simulation. We propose here a set-membership method based on interval analysis to detect different types of discontinuities. One of them is the sliding surface where the state trajectory jumps indefinitely between two distinct be- haviors. As an application, we consider the validation of a sailboat controller. We show that our approach is able to detect and explain some unwanted slid- ing effects that may be observed in rare and specific situations on our actual sailboat robots. - 12:00-12:30: Solicited talk 2
- Kostiantyn Potomkin: JuliaReach: a Toolbox for Set-Based Reachability
abstract
In this talk, we present JuliaReach, a toolbox for set-based reachability analysis of dynamical systems. JuliaReach consists of two main packages: Reachability, containing implementations of reachability algorithms for continuous and hybrid systems, and LazySets, a standalone library that implements state-of-the-art algorithms for calculus with convex sets. The library offers both concrete and lazy set representations, where the latter stands for the ability to delay set computations until they are needed. The choice of the programming language Julia and the accompanying documentation of our toolbox allow researchers to easily translate set-based algorithms from mathematics to software in a platform-independent way, while achieving runtime performance that is comparable to statically compiled languages. Combining lazy operations in high dimensions and explicit computations in low dimensions, JuliaReach can be applied to solve complex, large-scale problems. The talk is based on the following paper: Sergiy Bogomolov, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and Christian Schilling. JuliaReach: a toolbox for set-based reachability, HSCC 2019.
- 12:30 - 14:00: Break
- 14:00 - 15:00: Session 3:
- Industrial invited talk 2: Hermann Schichl: Optimization problems in the power market - to verify or not to verify
abstract
Energy production is a surprisingly complex problem with conflicting modeling paradigms. On the one hand, electricity is not storable, so the power network must be balanced at all times, on the other hand there are several technologies available to store energy - from small scale systems like batteries to huge pump storage water plants. The various primary energy sources like wind, sunlight, oil, coal, lignite, and water combined together with various legal regulations lead to unusual constraints and very complex non-linear optimization problems. Is it worthwhile to apply algorithms based on verified computing techniques like interval analysis, or are purely numerical heuristic approaches preferable? - 15:00 - 15:30: Break
- 15:30 - 17:25: Session 4:
-
- 15:30-16:00: Solicited talk 3:
- David Monniaux: Computing over convex polyhedra using VPL
abstract
Convex polyhedra occur in a variety of mathematical and computer science contexts, including static program analysis and some advanced compilation schemes. The usual approach to computing over them is the “dual description”, both as the convex hull of a set of generators (vertices, for bounded polyhedra) and as the solution of a system of linear equalities and inequalities (the constraints). This approach hasmany advantages but suffers from two drawbacks: the generator representation is exponential in the dimension in some common cases in program analysis (thus users tended to drastically limit the dimension), and it is difficult to check the final result without somehow checking the correctness of the full algorithm of conversion between descriptions. In contrast, with a constraint-only representation, it is possible to provide, along with each constraint of the result polyhedron, a certificate of its soundness. This is sufficient to certify that the computed result contains the ideal result, which is enough to certify that many program analyses are correct. In this talk I will discuss: – The “conventional” constraint-only algorithms based on Fourier-Motzkin elimination. – Our newer approach based on parametric linear programming. – How to obtain trustable, exact results from parallel efficient code implemented using floating-point arithmetic and untrusted solvers. – Other applications of parametric linear programming. You are welcome to download our library VPL (https://github.com/VERIMAG-Polyhedra/VPL) - 16:00-16:30: Solicited talk 4:
- Hoang-Dung Tran: Verification of Learning-Enabled Cyber-Physical Systems
abstract
Deep Neural Networks (DNNs) have been increasingly applied in safety-critical applications such as self- driving cars, unmanned underwater vehicles (UUV), and medical image diagnostics recently. The ability to learn sophisticated features and functions makes DNNs outstanding compared to other techniques in solving complicated tasks. At the same time, due to high nonlinearity, DNNs behaviors are generally unpredictable. Additionally, they are also vulnerable to adversarial attacks, where slightly changing in the input can cause a dramatic change in the output of a network. Since the failure of DNNs-based components in safety-critical systems can cause the loss of human lives, there is an urgent need for methods and tools to verify/certificate the safety and robustness of such systems. In this talk, I present a formal framework for verifying the safety and robustness of DNNs and learning-enabled Cyber-Physical Systems (CPS) using reachability analysis. The crux of our approach is a collection of reachability algorithms performing on novel geometrical set data structures that represent the bounded uncertainty of the input of a DNN or the initial conditions of a learning-enabled CPS efficiently. The proposed reachability algorithms construct a reachable set containing all possible outputs corresponding to the bounded uncertainty of a system. The reachable set is then used to reason about the safety or robustness of the systems. Our framework has been implemented in NNV, a neural network verification tool written in Matlab and Python that is gaining much attention from the research community and industry. Our generic framework has been tacked the following challenging subjects successfully: 1) safety and robustness verification of deep feed-forward neural networks (FNNs), 2) safety verification of neural-network-based control systems, 3) robustness verification of deep image classification convolutional neural networks (CNNs), 4) robustness verification of deep semantic segmentation networks (SSNs). - 16:30-17:00: Solicited talk 5:
- Sriram Sankaranarayanan: Reachability Analysis using Message Passing in Treewidth Bounded Systems
abstract
Reachability analysis for nonlinear systems often fails to scale due to the curse of dimensions. A common approach is to decompose the reachability problem for a system with numerous state variables into problems involving smaller number of variables through projection. In this talk, we will go over some recent results based on treewidth decompositions involving the dependency graph of the variables in a nonlinear system. We demonstrate how treewidth decomposition yields a tree of subsets of state variables. We introduce a message passing approach that can be used to refine tree decompositions, inspired by similar approaches for inference in Bayesian networks. We present some preliminary results and comparisons. This talk is based on a recent paper Sriram Sankaranarayanan, Reachability Analysis Using Message Passing over Tree Decompositions. CAV 2020: 604-628 - 17:00-17:25: Contributed talk 4
- Tommaso Dreossi, Giorgio Ballardin, Parth Gupta, Jan Bakus, Yu-Hsiang Lin and Vamsi Salaka: Analysis of E-commerce Ranking Signals via Signal Temporal Logic
abstract
The timed position of documents ranked by e-commerce websites can be seen as signals. Signals carry useful information such as drop or rise of documents over time or user behaviors. In this work, we propose to use the logic formalism called Signal Temporal Logic (STL) to characterize document behaviors in ranking accordingly to the specified formulas. Our analysis shows that interesting document behaviors can be easily formalized and detected thanks to STL formulas. We validate our idea on a dataset of 100K product signals. Through to the presented framework, we uncover interesting patterns, such as cold start, warm start, spikes, etc., and inspect how they affect our learning to ranks models.
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