GitHub

Bibliography

This page includes references to the scientific works that we have applied throughout this library. Although the list is not meant to be exhaustive, we think it should give a solid starting place for those who want to explore further.

If you use ReachabilityAnalysis.jl for your own work, please consider citing the appropriate original reference(s). We provide the BibTeX entries in each case.

If you find that a reference here is missing, if you spot a typo or want to update a reference, do not hesitate to contact us by email, or open an issue. Sorting is alphabetic.

[Alt10]
M. Althoff. Reachability analysis and its application to the safety assessment of autonomous cars. Ph.D. Thesis, Technische Universität München (2010).
[Alt20]
[ABF+19]
M. Althoff, S. Bak, M. Forets, G. Frehse, N. Kochdumper, R. Ray, C. Schilling and S. Schupp. ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics. In: Applied Verification of Continuous and Hybrid Systems (ARCH), Vol. 61 of EPiC Series in Computing, edited by G. Frehse and M. Althoff (EasyChair, 2019); pp. 14–40.
[AFG21]
[AGK18]
M. Althoff, D. Grebenyuk and N. Kochdumper. Implementation of Taylor models in CORA 2018. In: Applied Verification of Continuous and Hybrid Systems (ARCH), Vol. 54 of EPiC Series in Computing, edited by G. Frehse, M. Althoff, S. Bogomolov and T. T. Johnson (EasyChair, 2018); pp. 145–173.
[AKS11]
M. Althoff, B. H. Krogh and O. Stursberg. Analyzing reachability of linear dynamic systems with parametric uncertainties. Modeling, Design, and Simulation of Systems with Uncertainties, 69–94 (2011).
[ASB07]
[ASG01]
A. C. Antoulas, D. C. Sorensen and S. Gugercin. A survey of model reduction methods for large-scale systems. Contemporary Mathematics 280, 193–220 (2001).
[Bea08]
R. W. Beard. Quadrotor dynamics and control. Technical Report 1325 (Brigham Young University, 2008).
[BEKS17]
J. Bezanson, A. Edelman, S. Karpinski and V. B. Shah. Julia: A Fresh Approach to Numerical Computing. SIAM Review 59, 65–98 (2017).
[BFF+18]
S. Bogomolov, M. Forets, G. Frehse, F. Viry, A. Podelski and C. Schilling. Reach Set Approximation through Decomposition with Low-dimensional Sets and High-dimensional Matrices. In: Hybrid Systems: Computation and Control (HSCC), edited by M. Prandini and J. V. Deshmukh (ACM, 2018); pp. 41–50.
[CPPS06]
L. P. Carloni, R. Passerone, A. Pinto and A. L. Sangiovanni-Vincentelli. Languages and Tools for Hybrid Systems Design. Foundations and Trends in Electronic Design Automation 1 (2006).
[CM17]
N. Chan and S. Mitra. Verifying safety of an autonomous spacecraft rendezvous mission. In: Applied Verification of Continuous and Hybrid Systems (ARCH), Vol. 48 of EPiC Series in Computing, edited by G. Frehse and M. Althoff (EasyChair, 2017); pp. 20–32.
[C{S13]
X. Chen, E. Ábrahám and S. Sankaranarayanan. Flow: An Analyzer for Non-linear Hybrid Systems*. In: Computer Aided Verification (CAV), Vol. 8044 of LNCS, edited by N. Sharygina and H. Veith (Springer, 2013); pp. 258–263.
[Com03]
C. Combastel. A state bounding observer based on zonotopes. In: European Control Conference (ECC) (IEEE, 2003); pp. 2589–2594.
[FS22]
M. Forets and C. Schilling. Conservative Time Discretization: A Comparative Study. In: Integrated Formal Methods (iFM), Vol. 13274 of LNCS, edited by M. H. Beek and R. Monahan (Springer, 2022); pp. 149–167.
[FS21]
M. Forets and C. Schilling. Reachability of Weakly Nonlinear Systems Using Carleman Linearization. In: Reachability Problems (RP), Vol. 13035 of LNCS, edited by P. C. Bell, P. Totzke and I. Potapov (Springer, 2021); pp. 85–99.
[FLD+11]
G. Frehse, C. Le Guernic, A. Donzé, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang and O. Maler. SpaceEx: Scalable Verification of Hybrid Systems. In: Computer Aided Verification (CAV), Vol. 6806 of LNCS, edited by G. Gopalakrishnan and S. Qadeer (Springer, 2011); pp. 379–395.
[GSA+20]
L. Geretti, J. A. Sandretto, M. Althoff, L. Benet, A. Chapoutot, X. Chen, P. Collins, M. Forets, D. Freire, F. Immler, N. Kochdumper, D. P. Sanders and C. Schilling. ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics. In: Applied Verification of Continuous and Hybrid Systems (ARCH), Vol. 74 of EPiC Series in Computing (EasyChair, 2020); pp. 49–75.
[GSA+21]
L. Geretti, J. A. Sandretto, M. Althoff, L. Benet, A. Chapoutot, P. Collins, P. S. Duggirala, M. Forets, E. Kim, U. Linares, D. P. Sanders, C. Schilling and M. Wetzlinger. ARCH-COMP21 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics. In: Applied Verification of Continuous and Hybrid Systems (ARCH), Vol. 80 of EPiC Series in Computing, edited by G. Frehse and M. Althoff (EasyChair, 2021); pp. 32–54.
[Gir05]
A. Girard. Reachability of Uncertain Linear Systems Using Zonotopes. In: Hybrid Systems: Computation and Control (HSCC), Vol. 3414 of LNCS, edited by M. Morari and L. Thiele (Springer, 2005); pp. 291–305.
[GL08]
A. Girard and C. Le Guernic. Efficient reachability analysis for linear systems using support functions. IFAC Proceedings Volumes 41, 8966–8971 (2008).
[GLM06]
A. Girard, C. Le Guernic and O. Maler. Efficient Computation of Reachable Sets of Linear Time-Invariant Systems with Inputs. In: Hybrid Systems: Computation and Control (HSCC), Vol. 3927 of LNCS, edited by J. P. Hespanha and A. Tiwari (Springer, 2006); pp. 257–271.
[GCL+20]
S. Gruenbacher, J. Cyranka, M. Lechner, M. A. Islam, S. A. Smolka and R. Grosu. Lagrangian Reachtubes: The Next Generation. In: Conference on Decision and Control (CDC) (IEEE, 2020); pp. 1556–1563.
[Hig08]
[Klu20]
C. A. Kluever. Dynamic Systems: Modeling, Simulation, and Control (John Wiley & Sons, 2020).
[KM18]
S. Kopecz and A. Meister. On order conditions for modified Patankar–Runge–Kutta schemes. Applied Numerical Mathematics 123, 159–179 (2018).
[LL98]
M. T. Laub and W. F. Loomis. A molecular network that produces spontaneous oscillations in excitable cells of Dictyostelium. Molecular Biology of the Cell 9, 3521–3532 (1998).
[LG10]
[LG09]
C. Le Guernic and A. Girard. Reachability Analysis of Hybrid Systems Using Support Functions. In: Computer Aided Verification (CAV), Vol. 5643 of LNCS, edited by A. Bouajjani and O. Maler (Springer, 2009); pp. 540–554.
[Moo65]
R. E. Moore. Automatic local coordinate transformations to reduce the growth of error bounds in interval computation of solutions of ordinary differential equations. Error in Digital Computation 2, 103–140 (1965).
[Sch18]
C. Schilling. Fundamental techniques for the scalable analysis of systems. Ph.D. Thesis, University of Freiburg, Germany (2018).
[SO15]
T. Strathmann and J. Oehlerking. Verifying Properties of an Electro-Mechanical Braking System. In: Applied Verification of Continuous and Hybrid Systems (ARCH), Vol. 34 of EPiC Series in Computing, edited by G. Frehse and M. Althoff (EasyChair, 2015); pp. 49–56.
[TD13]
R. Testylier and T. Dang. NLTOOLBOX: A Library for Reachability Computation of Nonlinear Dynamical Systems. In: Automated Technology for Verification and Analysis (ATVA), Vol. 8172 of LNCS, edited by D. V. Hung and M. Ogawa (Springer, 2013); pp. 469–473.
[TNJ16]
H.-D. Tran, L. V. Nguyen and T. T. Johnson. Large-Scale Linear Systems from Order-Reduction. In: Applied Verification of Continuous and Hybrid Systems (ARCH), Vol. 43 of EPiC Series in Computing, edited by G. Frehse and M. Althoff (EasyChair, 2016); pp. 60–67.
[YS18]
[ACH+95]
R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis and S. Yovine. The Algorithmic Analysis of Hybrid Systems. Theoretical Computer Science 138, 3–34 (1995).
[BFF+20]
[Che15]
X. Chen. Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models. Ph.D. Thesis, RWTH Aachen, Germany (2015).
[Fre16]
G. Frehse. Scalable Verification of Hybrid Systems (Verimag, 2016).
[FR12]
G. Frehse and R. Ray. Flowpipe-Guard Intersection for Reachability Computations with Support Functions. In: Analysis and Design of Hybrid Systems (ADHS), Vol. 45 no. 9 of IFAC Proceedings Volumes, edited by M. Heemels and B. D. Schutter (Elsevier, 2012); pp. 94–101.
[Gir04]
A. Girard. Algorithmic Analysis of Hybrid Systems. Ph.D. Thesis, Grenoble Institute of Technology, France (2004).
[Gir13]
A. Girard. Computational Approaches to Analysis and Control of Hybrid Systems (University of Grenoble, 2013).
[HB19]
V. S. Hakim and M. J. Bekooij. Reachability Analysis of Hybrid Automata with Clocked Linear Dynamics. In: Software and Compilers for Embedded Systems (SCOPES), edited by S. Stuijk (ACM, 2019); pp. 27–36.
[Jol11]
M. Joldes. Rigorous Polynomial Approximations and Applications. Ph.D. Thesis, École normale supérieure de Lyon, France (2011).
[Kek18]
N. Kekatos. Formal Verification of Cyber-Physical Systems in the Industrial Model-Based Design Process. Ph.D. Thesis, Grenoble Alpes University, France (2018).
[Le 09]
C. Le Guernic. Reachability Analysis of Hybrid Systems with Linear Continuous Dynamics. Ph.D. Thesis, Joseph Fourier University, Grenoble, France (2009).
[Ray12]
R. Ray. Reachability Analysis of Hybrid Systems using Support Functions. Ph.D. Thesis, Grenoble Alpes University, France (2012).
[Roc18]
A. Rocca. Formal methods for modelling and validation of biological models. Ph.D. Thesis, Grenoble Alpes University, France (2018).
[Sch19]
[XFZ18]
B. Xue, M. Fränzle and N. Zhan. Under-Approximating Reach Sets for Polynomial Continuous Systems. In: Hybrid Systems: Computation and Control (HSCC), edited by M. Prandini and J. V. Deshmukh (ACM, 2018); pp. 51–60.