LazySets.jl

The articles appear in reverse chronological order.

[18] Reachability of weakly nonlinear systems using Carleman linearization. Marcelo Forets and Christian Schilling. arXiv preprint arXiv:2108.10390 (2021). Accepted in: 15th International Conference on Reachability Problems (2021). October 25-27 2021, Liverpool, UK.

[17] Combined Exact and Heuristics Based Approach to Hamiltonian Path Problem Optimization for Route Planning. Fernando Hernandez, Rafael Sotelo and Marcelo Forets (2021). In Winkenbach, M., Parks, S., & Noszek, J. (Eds.), Technical Proceedings of the 2021 Amazon Last Mile Routing Research Challenge (pp. XXI.1–XXI.12). MIT Libraries.

[16] ARCH-COMP21 Category Report: Artificial Intelligence and Neural Network Controlled Systems for Continuous and Hybrid Systems Plants. Taylor T. Johnson, Diego Manzanas Lopez, Luis Benet, Marcelo Forets, Christian Schilling, Radoslav Ivanov, Taylor Carpenter, James Weimer, and Insup Lee. (2021) ARCH21. 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21).

[15] ARCH-COMP21 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics. Matthias Althoff, Erika Abraham, Marcelo Forets, Goran Frehse, Daniel Freire, Christian Schilling, Stefan Schupp, and Mark Wetzlinger. (2021) ARCH21. 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21).

[14] ARCH-COMP21 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics. Luca Geretti, Julien Alexandre dit Sandretto, Matthias Althoff, Luis Benet, Alexandre Chapoutot, Pieter Collins, Parasara Sridhar Duggirala, Marcelo Forets, Edward Kim, Uziel Linares, David P. Sanders, Christian Schilling, and Mark Wetzlinger. (2021) ARCH21. 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21).

[13] 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).

[12] Synthesis of hybrid automata with affine dynamics from time-series data. García Soto, Miriam, Thomas A. Henzinger, and Christian Schilling. HSCC (2021). doi: 10.1145/3447928.3456704. Get pdf from arXiv: 2102.12734

[11] Efficient reachability analysis of parametric linear hybrid systems with time-triggered transitions. Marcelo Forets, Daniel Freire, Christian Schilling, 2020. arXiv: 2006.12325. 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 (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. 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. HSCC: 22nd ACM International Conference on Hybrid Systems: Computation and Control, 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 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.

• ReachabilityAnalysis.jl -- Methods to compute sets of states reachable by dynamical systems.
• NeuralNetworkAnalysis.jl -- Methods to verify neural network controlled systems using reachability analysis
• NeuralVerification.jl -- Methods to soundly verify deep neural networks.
• InvariantSets.jl -- Compute, approximate and display invariant sets.
• OpticSim.jl -- Ray tracing for procedurally generated systems.
• Photometry.jl -- Utilities for characterizing sources in astronomical images.
• Swalbe.jl -- Simple Julia Lattice Boltzmann Solver for Thin Liquid Films and Droplets
• IntervalLinearAlgebra.jl -- Routines to perform numerical linear algebra using interval arithmetic

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