LazySets.jl

In reverse chronological order,

[12] Combining Set Propagation with Finite Element Methods for Time Integration in Transient Solid Mechanics Problems. Forets, Marcelo, Daniel Freire Caporale, and Jorge M. Pérez Zerpa.. arXiv preprint arXiv:2105.05841 (2021).

[11] Efficient reachability analysis of parametric linear hybrid systems with time-triggered transitions. Marcelo Forets, Daniel Freire, Christian Schilling, 2020. arXiv: 2006.12325. Published in 18th ACM-IEEE International Conference on Formal Methods and Models for System Design . See conference page.

[10] ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics. Matthias Althoff, Stanley Bak, Zongnan Bao, Marcelo Forets, Daniel Freire, Goran Frehse, Niklas Kochdumper, Yangge Li, Sayan Mitra, Rajarshi Ray, Christian Schilling, Stefan Schupp, and Mark Wetzlinger (2020) ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), vol 74, pages 16--48. 10.29007/7dt2.

[9] ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics. Luca Geretti, Julien Alexandre dit Sandretto, Matthias Althoff, Luis Benet, Alexandre Chapoutot, Xin Chen, Pieter Collins, Marcelo Forets, Daniel Freire, Fabian Immler, Niklas Kochdumper, David P. Sanders and Christian Schilling (2020) ARCH20. To appear in 7th International Workshop on Applied Verification of Continuous and Hybrid Systems. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), vol 74, pages 49--75. 10.29007/zkf6.

[8] Case Study: Reachability Analysis of a unified Combat-Command-and-Control Model. Sergiy Bogomolov, Marcelo Forets, Kostiantyn Potomkin. International Conference on Reachability Problems (2020). Lecture Notes in Computer Science, vol 12448. (2020) doi: 10.1007/978-3-030-61739-4_4. Presented in the 14th International Conference on Reachability Problems 2020. article

[7] Reachability analysis of linear hybrid systems via block decomposition. Sergiy Bogomolov, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, Christian Schilling. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 39:11 (2020). doi: 10.1109/TCAD.2020.3012859. Presented in Embedded Systems Week 2020. Get pdf from arXiv: 1905.02458.

[6] Algorithms for verifying deep neural networks. Liu, C., Arnon, T., Lazarus, C., Barrett, C., & Kochenderfer, M. J. (2019). Get pdf from arXiv: 1903.06758.

[5] ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics. Matthias Althoff, Stanley Bak, Marcelo Forets, Goran Frehse, Niklas Kochdumper, Rajarshi Ray, Christian Schilling and Stefan Schupp (2019) ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, vol 61, pages 14--40 doi: 10.29007/bj1w.

[4] ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics. Fabian Immler, Matthias Althoff, Luis Benet, Alexandre Chapoutot, Xin Chen, Marcelo Forets, Luca Geretti, Niklas Kochdumper, David P. Sanders and Christian Schilling (2019) ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, vol 61, pages 41--61 doi: 10.29007/bj1w.

[3] JuliaReach: a Toolbox for Set-Based Reachability. Sergiy Bogomolov, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, Christian Schilling. Published in Proceedings of HSCC'19: 22nd ACM International Conference on Hybrid Systems: Computation and Control (HSCC'19), see ACM link here. Get pdf from arXiv: 1901.10736.

[2] ARCH-COMP18 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics. Matthias Althoff, Stanley Bak, Xin Chen, Chuchu Fan, Marcelo Forets, Goran Frehse, Niklas Kochdumper, Yangge Li, Sayan Mitra, Rajarshi Ray, Christian Schilling and Stefan Schupp (2018) ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems, 54: 23–52. doi: 10.29007/73mb.

[1] Reach Set Approximation through Decomposition with Low-dimensional Sets and High-dimensional Matrices. Sergiy Bogomolov, Marcelo Forets, Goran Frehse, Frédéric Viry, Andreas Podelski and Christian Schilling (2018) HSCC'18 Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control: 41–50. See the ACM Digital Library link, or the arXiv: 1801.09526.

We present JuliaReach, a Julia ecosystem to perform reachability analysis of dynamical systems. JuliaReach builds on sound scientific approaches and was, in two occasions (2018 and 2020) the winner of the annual friendly competition on Applied Verification for Continuous and Hybrid Systems (ARCH-COMP).

The workshop consists of three parts (respectively packages) in JuliaReach: our core package for set representations, our main package for reachability analysis, and a new package applying reachability analysis with potential use in domain of control, robotics and autonomous systems.

In the first part we present LazySets.jl, which provides ways to symbolically represent sets of points as geometric shapes, with a special focus on convex sets and polyhedral approximations. LazySets.jl provides methods to apply common set operations, convert between different set representations, and efficiently compute with sets in high dimensions.

In the second part we present ReachabilityAnalysis.jl, which provides tools to approximate the set of reachable states of systems with both continuous and mixed discrete-continuous dynamics, also known as hybrid systems. It implements conservative discretization and set-propagation techniques at the state-of-the-art.

In the third part we present NeuralNetworkAnalysis.jl, which is an application of ReachabilityAnalysis.jl to analyze dynamical systems that are controlled by neural networks. This package can be used to validate or invalidate specifications, for instance about the safety of such systems.

Workshop materials are available here: https://github.com/JuliaReach/JuliaCon-2021-Workshop-Its-All-Set