arXiv:2101.05256v1 [cs.LO] 1 Jan 2021

DOI: 10.4204/EPTCS.331
ISSN: 2075-2180


Proceedings 6th International Workshop on
Symbolic-Numeric methods for Reasoning about CPS and IoT
online, 31 August 2020

Edited by: Thao Dang and Stefan Ratschan

Thao Dang and Stefan Ratschan
Invited Tutorial: Solving non-linear arithmetic with SAT modulo theories and abstraction
Alberto Griggio
Invited Industrial Talk: Optimization problems in the power market - to verify or not to verify
Hermann Schichl
Interval centred form for proving stability of non-linear discrete-time systems
Auguste Bourgois and Luc Jaulin
Verification and Reachability Analysis of Fractional-Order Differential Equations Using Interval Analysis
Andreas Rauh and Julia Kersten
Analysis of E-commerce Ranking Signals via Signal Temporal Logic
Tommaso Dreossi, Giorgio Ballardin, Parth Gupta, Jan Bakus, Yu-Hsiang Lin and Vamsi Salaka
Enclosing the Sliding Surfaces of a Controlled Swing
Luc Jaulin and Benoît Desrochers


Welcome to the proceedings of the 6th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR 2020). The workshop was planned to take place in Vienna, Austria as a satellite event of QONFEST'20. Due to the COVID-19 pandemic, the whole event took place online.

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 for these systems. The synergy between symbolic and numerical approaches is fruitful thanks to their complementarity:

The workshop program consisted of an invited industrial talk by Hermann Schichl (DAGOPT and University of Vienna), an invited tutorial by Alberto Griggio (Fondazione Bruno Kessler), four contributed talks, and five talks that the program chairs solicited from additional speakers.

The proceedings contain three papers underlying contributed talks, and one paper that extends the work presented in a solicited talk. All papers were reviewed by the program committee that consisted of the following members:

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)

The organization of SNR 2020 would not have been possible without the combined efforts of many individuals who contributed their share under the difficult circumstances of the COVID-19 pandemic. Especially, we thank the workshop speakers and authors for presenting their research at SNR and the participants for contributing in the discussions. We are grateful to the QONFEST organizers for making the online event run smoothly. Finally, we thank the PC members for their work in ensuring the quality of the contributions, and the SNR Steering Committee: Erika Ábrahám, Sergiy Bogomolov, Martin Fränzle, Taylor T. Johnson and Ashish Tiwari for their advice and support.

We also refer to readers to the proceedings of the previous edition of the workshop, SNR 2019.

Solving non-linear arithmetic with SAT modulo theories and abstraction

Alberto Griggio (Fondazione Bruno Kessler)

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

Hermann Schichl (DAGOPT, University of Vienna)

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?