Fully-Automated Verification of Linear Systems Using Reachability Analysis with Support Functions

Autor: Mark Wetzlinger, Niklas Kochdumper, Stanley Bak, Matthias Althoff

Publikováno v: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control.

While reachability analysis is one of the major techniques for formal verification of dynamical systems, the requirement to adequately tune algorithm parameters often prevents its widespread use in practical applications. In this work, we fully autom

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0f54101d8a4197207ed3e1e476d69346
https://doi.org/10.1145/3575870.3587121

ARCH-COMP22 category report: Continuous and hybrid systems with nonlinear dynamics

Autor: Luca Geretti, Julien Alexandre Dit Sandretto, Matthias Althoff, Luis Benet, Pieter Collins, Parasara Duggirala, Marcelo Forets, Edward Kim, Stefan Mitsch, Christian Schilling, Mark Wetzlinger

Publikováno v: Geretti, L, Alexandre Dit Sandretto, J, Althoff, M, Benet, L, Collins, P, Duggirala, P S, Forets, M, Kim, E, Mitsch, S, Schilling, C & Wetzlinger, M 2022, ARCH-COMP22 category report: Continuous and hybrid systems with nonlinear dynamics . in G Frehse, M Althoff, E Schoitsch & J Guiochet (eds), 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22) . EasyChair, EPiC Series in Computing, vol. 90, pp. 58-85, 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22), Munich, Germany, 06/09/2022 . https://doi.org/10.29007/fnzc

We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid S

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::433d8ae018629c63bc2c4dfc7b11d3d0
https://vbn.aau.dk/da/publications/7b2bc7c4-95bb-487b-a2f4-ee56118e8e5a

ARCH-COMP21 Category Report:Continuous and Hybrid Systems with Linear Continuous Dynamics

Autor: Matthias Althoff, Erika Ábrahám, Marcelo Forets, Goran Frehse, Daniel Freire, Christian Schilling, Stefan Schupp, Mark Wetzlinger

Publikováno v: Althoff, M, Ábrahám, E, Forets, M, Frehse, G, Freire, D, Schilling, C, Schupp, S & Wetzlinger, M 2021, ARCH-COMP21 Category Report : Continuous and Hybrid Systems with Linear Continuous Dynamics . in G Frehse & M Althoff (eds), 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21) . EasyChair, EPiC Series in Computing, vol. 80, pp. 1-31, 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), Bruxelles, Belgium, 09/07/2021 . https://doi.org/10.29007/lhbw

We present the results of the ARCH1 2021 friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. In its fifth edition, four tools have been applied to solve nine different benchmark problems in t

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::384ae16454900a77c2e9fdc90c27f7ee
https://vbn.aau.dk/da/publications/4cbf4436-8097-4c32-8563-5c6e3e093576

Adaptive parameter tuning for reachability analysis of nonlinear systems

Autor: Adrian Kulmburg, Matthias Althoff, Mark Wetzlinger

Publikováno v: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control
HSCC
Proc.of the 24th International Conference on Hybrid Systems: Computation and Control

Reachability analysis fails to produce tight reachable sets if certain algorithm parameters are poorly tuned, such as the time step size or the accuracy of the set representation. The tuning is especially difficult in the context of nonlinear systems

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6b6575c59369fab6f36d2af926b029b8