LazySets.jl

LazySets is a Julia package for calculus with convex sets.

🎯 Resources

• Manual
• Contributing
• Release notes of tagged versions
• Release notes of the development version
• Developers

💾 Installing

LazySets.jl is a registered Julia package and as such you can install it by activating the pkg mode (type ], and to leave it, type <backspace>), followed by

pkg> add LazySets

See the Getting started section of the manual for other options.

📘 Publications

This library has been applied in a number of scientic works. In reverse chronological order,

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

[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.

🌍 Ecosystem

LazySets.jl is applied in a number of projects in the Julia technical computing stack:

• ReachabilityAnalysis.jl -- Methods to compute sets of states reachable by dynamical systems.
• NeuralVerification.jl -- Methods to soundly verify deep neural networks.
• Photometry.jl -- Utilities for characterizing sources in astronomical images.
• InvariantSets.jl -- Compute, approximate and display invariant sets.