SpaceEx

SpaceEx: Scalable Verification of Hybrid Systems. We present a scalable reachability algorithm for hybrid systems with piecewise affine, non-deterministic dynamics. It combines polyhedra and support function representations of continuous sets to compute an over-approximation of the reachable states. The algorithm improves over previous work by using variable time steps to guarantee a given local error bound. In addition, we propose an improved approximation model, which drastically improves the accuracy of the algorithm. The algorithm is implemented as part of SpaceEx, a new verification platform for hybrid systems, available at spaceex.imag.fr. Experimental results of full fixed-point computations with hybrid systems with more than 100 variables illustrate the scalability of the approach.


References in zbMATH (referenced in 73 articles )

Showing results 1 to 20 of 73.
Sorted by year (citations)

1 2 3 4 next

  1. Cassez, Franck; Jensen, Peter Gjøl; Guldstrand, Larsen Kim: Verification and parameter synthesis for real-time programs using refinement of trace abstraction (2021)
  2. Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel: Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration (2021)
  3. Fahrenberg, Uli; Legay, Axel; Quaas, Karin: Computing branching distances with quantitative games (2020)
  4. García Soto, Miriam; Prabhakar, Pavithra: Abstraction based verification of stability of polyhedral switched systems (2020)
  5. Goyal, Manish; Duggirala, Parasara Sridhar: Extracting counterexamples induced by safety violation in linear hybrid systems (2020)
  6. Malik, Avinash; Roop, Partha: A dynamic quantized state system execution framework for hybrid automata (2020)
  7. Suenaga, Kohei; Ishizawa, Takuya: Generalized property-directed reachability for hybrid systems (2020)
  8. Sun, Hao; Li, Junfeng: Analysis on reachable set for spacecraft relative motion under low-thrust (2020)
  9. Tsachouridis, Vassilios A.; Giantamidis, Georgios; Basagiannis, Stylianos; Kouramas, Kostas: Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers (2020)
  10. Bogomolov, Sergiy; Forets, Marcelo; Frehse, Goran; Potomkin, Kostiantyn; Schilling, Christian: JuliaReach: a toolbox for set-based reachability (2019)
  11. Gronski, Jessica; Ben Sassi, Mohamed-Amin; Becker, Stephen; Sankaranarayanan, Sriram: Template polyhedra and bilinear optimization (2019)
  12. Meyer, Pierre-Jean; Devonport, Alex; Arcak, Murat: TIRA: toolbox for interval reachability analysis (2019)
  13. Sánchez, César; Schneider, Gerardo; Ahrendt, Wolfgang; Bartocci, Ezio; Bianculli, Domenico; Colombo, Christian; Falcone, Yliès; Francalanza, Adrian; Krstić, Srđan; Lourenço, João M.; Nickovic, Dejan; Pace, Gordon J.; Rufino, Jose; Signoles, Julien; Traytel, Dmitriy; Weiss, Alexander: A survey of challenges for runtime verification from advanced application domains (beyond software) (2019)
  14. Sogokon, Andrew; Jackson, Paul B.; Johnson, Taylor T.: Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants (2019)
  15. Tran, Hoang-Dung; Nguyen, Luan Viet; Hamilton, Nathaniel; Xiang, Weiming; Johnson, Taylor T.: Reachability analysis for high-index linear differential algebraic equations (2019)
  16. Bogomolov, Sergiy; Forets, Marcelo; Frehse, Goran; Viry, Frédéric; Podelski, Andreas; Schilling, Christian: Reach set approximation through decomposition with low-dimensional sets and high-dimensional matrices (2018)
  17. Chen, Mo; Herbert, Sylvia L.; Vashishtha, Mahesh S.; Bansal, Somil; Tomlin, Claire J.: Decomposition of reachable sets and tubes for a class of nonlinear systems (2018)
  18. Doyen, Laurent; Frehse, Goran; Pappas, George J.; Platzer, André: Verification of hybrid systems (2018)
  19. Drechsler, Rolf (ed.): Formal system verification. State-of the-art and future trends (2018)
  20. Le Coënt, Adrien; dit Sandretto, Julien Alexandre; Chapoutot, Alexandre; Fribourg, Laurent: An improved algorithm for the control synthesis of nonlinear sampled switched systems (2018)

1 2 3 4 next


Further publications can be found at: http://spaceex.imag.fr/documentation/publications