dReach

dReach:(δ)-reachability analysis for hybrid systems. dReach is a bounded reachability analysis tool for nonlinear hybrid systems. It encodes reachability problems of hybrid systems to first-order formulas over real numbers, which are solved by delta-decision procedures in the SMT solver dReach. In this way, dReach is able to handle a wide range of highly nonlinear hybrid systems. It has scaled well on various realistic models from biomedical and robotics applications.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 19 articles )

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

  1. Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico: On checking equivalence of simulation scripts (2021)
  2. Abhishek, Aakash; Sood, Harry; Jeannin, Jean-Baptiste: Formal verification of braking while swerving in automobiles (2020)
  3. Goncharov, Sergey; Neves, Renato; Proença, José: Implementing hybrid semantics: from functional to imperative (2020)
  4. Yang, Zhengfeng; Wu, Min; Lin, Wang: An efficient framework for barrier certificate generation of uncertain nonlinear hybrid systems (2020)
  5. Islam, Md. Ariful; Cleaveland, Rance; Fenton, Flavio H.; Grosu, Radu; Jones, Paul L.; Smolka, Scott A.: Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans (2019)
  6. 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)
  7. Sogokon, Andrew; Jackson, Paul B.; Johnson, Taylor T.: Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants (2019)
  8. 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)
  9. Li, Yinan; Liu, Jun: ROCS: a robustly complete control synthesis tool for nonlinear dynamical systems (2018)
  10. Moggi, Eugenio; Farjudian, Amin; Duracz, Adam; Taha, Walid: Safe & robust reachability analysis of hybrid systems (2018)
  11. Navarro-López, E. M.; O’Toole, M. D.: Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties (2018)
  12. Bak, Stanley; Bogomolov, Sergiy; Althoff, Matthias: Time-triggered conversion of guards for reachability analysis of hybrid automata (2017)
  13. Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto: Invariant checking of NRA transition systems via incremental reduction to LRA with EUF (2017)
  14. Dreossi, Tommaso: Sapo: reachability computation and parameter synthesis of polynomial dynamical systems (2017)
  15. Dreossi, Tommaso; Dang, Thao; Piazza, Carla: Reachability computation for polynomial dynamical systems (2017)
  16. Figueiredo, Daniel; Martins, Manuel A.; Chaves, Madalena: Applying differential dynamic logic to reconfigurable biological networks (2017)
  17. Fulton, Nathan; Mitsch, Stefan; Bohrer, Brandon; Platzer, André: Bellerophon: tactical theorem proving for hybrid systems (2017)
  18. Sandler, Andrei; Tveretina, Olga: ParaPlan: a tool for parallel reachability analysis of planar polygonal differential inclusion systems (2017)
  19. Gan, Ting; Chen, Mingshuai; Dai, Liyun; Xia, Bican; Zhan, Naijun: Decidability of the reachability for a family of linear vector fields (2015)