LazySets.jl

Scalable Symbolic-Numeric Set Computations

| Introduction & Documentation | Status | Community | Version-Specific Citation | License | |:--------------------------------:|:----------:|:-------------:|:-----------------------------:|:-----------:| | | | | | |

❓ Introduction

The following article showcases the basic functionality, highlighting some of the key design choices:

Forets, Marcelo, and Christian Schilling. LazySets.jl: Scalable Symbolic-Numeric Set Computations. Proceedings of the JuliaCon Conferences (2021).

See below for how to cite it.

🎯 Resources

• Manual
• Release notes of the development version
• Release notes of previous versions
• How to contribute
• Developers team

💾 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 scientific works.

<details> <summary>Click to see the full list of publications that use LazySets.</summary>

The articles appear in reverse chronological order.

[33] Verified propagation of imprecise probabilities in non-linear ODEs. Ander Gray, Marcelo Forets, Christian Schilling, Scott Ferson, and Luis Benet (2024). International Journal of Approximate Reasoning, vol. 164. doi: 10.1016/j.ijar.2023.109044.

[32] Safety verification of decision-tree policies in continuous time. Christian Schilling, Anna Lukina, Emir Demirović, and Kim G. Larsen (2023). 37th Conference on Neural Information Processing Systems (NeurIPS). pdf.

[31] Shielded reinforcement learning for hybrid systems. Asger H. Brorholt, Peter G. Jensen, Kim G. Larsen, Florian Lorber, and Christian Schilling (2023). 1st International Conference on Bridging the Gap between AI and Reality (AISoLA), LNCS, vol. 14380, pp. 33-54. doi: 10.1007/978-3-031-46002-9_3, arXiv: 2308.14424.

[30] The inverse problem for neural networks. Marcelo Forets and Christian Schilling (2023). 1st International Conference on Bridging the Gap between AI and Reality (AISoLA), LNCS, vol. 14380, pp. 241-255. doi: 10.1007/978-3-031-46002-9_14, arXiv: 2308.14093.

[29] ARCH-COMP23 category report: Continuous and hybrid systems with linear continuous dynamics. Matthias Althoff, Marcelo Forets, Yangge Li, Sayan Mitra, Christian Schilling, Mark Wetzlinger, and Daniel Zhuang (2023). 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH23), vol 96, pp. 34-60. doi: 10.29007/nl86.

[28] ARCH-COMP23 category report: Continuous and hybrid systems with nonlinear dynamics. Luca Geretti, Julien Alexandre Dit Sandretto, Matthias Althoff, Luis Benet, Pieter Collins, Marcelo Forets, Elena Ivanova, Yangge Li, Sayan Mitra, Stefan Mitsch, Christian Schilling, Mark Wetzlinger, and Daniel Zhuang (2023). 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH23), vol 96, pp. 61-88. doi: 10.29007/93f2.

[27] ARCH-COMP23 category report: Artificial intelligence and neural network control systems for continuous and hybrid systems plants. Diego Manzanas Lopez, Matthias Althoff, Marcelo Forets, Taylor T. Johnson, Tobias Ladner, and Christian Schilling (2023). 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH23), vol 96, pp. 89-125. doi: 10.29007/x38n.

[26] ARCH-COMP22 category report: Continuous and hybrid systems with linear continuous dynamics. Matthias Althoff, Marcelo Forets, Christian Schilling, and Mark Wetzlinger (2022). 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22), vol 90, pp. 58-85. doi: 10.29007/mmzc.

[25] ARCH-COMP22 category report: Continuous and hybrid systems with nonlinear dynamics. Luca Geretti, Julien Alexandre Dit Sandretto, Matthias Althoff, Luis Benet, Pieter Collins, Parasara Sridhar Duggirala, Marcelo Forets, Edward Kim, Stefan Mitsch, Christian Schilling, and Mark Wetzlinger (2022). 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22), vol 90, pp. 86-112. doi: 10.29007/fnzc.

[24] ARCH-COMP22 category report: Artificial intelligence and neural network control systems for continuous and hybrid systems plants. Diego Manzanas Lopez, Matthias Althoff, Luis Benet, Xin Chen, Jiameng Fan, Marcelo Forets, Chao Huang, Taylor T. Johnson, Tobias Ladner, Wenchao Li, Christian Schilling, and Qi Zhu (2022). 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22), vol 90, pp. 142-184. doi: 10.29007/wfgr.

[23] Synthesis of parametric hybrid automata from time series. Miriam García Soto, Thomas A. Henzinger, and Christian Schilling (2022). Proceedings of the 20th International Symposium on Automated Technology for Verification and Analysis, LNCS, vol. 13505, pp. 337-353. doi: 10.1007/978-3-031-19992-9_22, arXiv: 2208.06383.

[22] Decomposing reach set computations with low-dimensional sets and high-dimensional matrices (extended version). Sergiy Bogomolov, Marcelo Forets, Goran Frehse, Andreas Podelski, and Christian Schilling (2022). Information and Computation, vol. 289. doi: 10.1016/j.ic.2022.104937.

[21] Conservative Time Discretization: A Comparative Study. Marcelo Forets and Christian Schilling (2022). Proceedings of the 17th International Conference on integrated Formal Methods (iFM), LNCS, vol. 13274, pp. 149-167. doi: 10.1007/978-3-031-07727-2_9, arXiv: 2111.01454.

[20] Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes. Christian Schilling, Marcelo Forets, and Sebastián Guadalupe (2022). Proceedings of the 36th Conference on Artificial Intelligence (AAAI). doi: 10.1609/aaai.v36i7.20790.

[19] **Combining Set Propagation with