arXiv:2101.05256v1 [cs.LO] 1 Jan 2021
|Preface 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||1|
|Verification and Reachability Analysis of Fractional-Order Differential Equations Using Interval Analysis Andreas Rauh and Julia Kersten||18|
|Analysis of E-commerce Ranking Signals via Signal Temporal Logic Tommaso Dreossi, Giorgio Ballardin, Parth Gupta, Jan Bakus, Yu-Hsiang Lin and Vamsi Salaka||33|
|Enclosing the Sliding Surfaces of a Controlled Swing Luc Jaulin and Benoît Desrochers||43|
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)
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.
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.
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?