In 1995, HyTech broke new ground as a potentially powerful tool for verifying hybrid systems – yet it has remained severely limited in its applicability to more complex systems. We address the main problems of HyTech with PHAVer, a new tool for the exact verification of safety properties of hybrid systems with piecewise constant bounds on the derivatives. Affine dynamics are handled by on-the-fly overapproximation and by partitioning the state space based on user-definable constraints and the dynamics of the system. PHAVer’s exact arithmetic is robust due to the use of the Parma Polyhedra Library, which supports arbitrarily large numbers. To manage the complexity of the polyhedral computations, we propose methods to conservatively limit the number of bits and constraints of polyhedra. Experimental results for a navigation benchmark and a tunnel diode circuit show the effectiveness of the approach.

References in zbMATH (referenced in 113 articles , 1 standard article )

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

1 2 3 4 5 6 next

  1. Bacci, Giovanni; Bouyer, Patricia; Fahrenberg, Uli; Larsen, Kim G.; Markey, Nicolas; Reynier, Pierre-Alain: Optimal and robust controller synthesis using energy timed automata with uncertainty (2021)
  2. Becchi, Anna; Zaffanella, Enea: PPLite: zero-overhead encoding of NNC polyhedra (2020)
  3. Yang, Jung-Min; Moor, Thomas; Raisch, Jörg: Refinements of behavioural abstractions for the supervisory control of hybrid systems (2020)
  4. 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)
  5. Doyen, Laurent; Frehse, Goran; Pappas, George J.; Platzer, André: Verification of hybrid systems (2018)
  6. Drechsler, Rolf (ed.): Formal system verification. State-of the-art and future trends (2018)
  7. Majumdar, Rupak; Raskin, Jean-François: Symbolic model checking in non-Boolean domains (2018)
  8. Nasti, Lucia; Milazzo, Paolo: A hybrid automata model of social networking addiction (2018)
  9. Zhang, Hui; Wu, Jinzhao: Formal verification and quantitative metrics of MPSoC data dynamics (2018)
  10. Bak, Stanley; Bogomolov, Sergiy; Althoff, Matthias: Time-triggered conversion of guards for reachability analysis of hybrid automata (2017)
  11. Bak, Stanley; Duggirala, Parasara Sridhar: Rigorous simulation-based analysis of linear hybrid systems (2017)
  12. Bogomolov, Sergiy; Frehse, Goran; Giacobbe, Mirco; Henzinger, Thomas A.: Counterexample-guided refinement of template polyhedra (2017)
  13. Dreossi, Tommaso; Dang, Thao; Piazza, Carla: Reachability computation for polynomial dynamical systems (2017)
  14. Fulton, Nathan; Mitsch, Stefan; Bohrer, Brandon; Platzer, André: Bellerophon: tactical theorem proving for hybrid systems (2017)
  15. Baştuğ, Mert; Petreczky, Mihály; Wisniewski, Rafael; Leth, John: Reachability and observability reduction for linear switched systems with constrained switching (2016)
  16. Colvin, Robert J.: Modelling and analysing neural networks using a hybrid process algebra (2016)
  17. Papadopoulos, Alessandro Vittorio; Prandini, Maria: Model reduction of switched affine systems (2016)
  18. Sankaranarayanan, Sriram: Change-of-bases abstractions for non-linear hybrid systems (2016)
  19. Aréchiga, Nikos; Kapinski, James; Deshmukh, Jyotirmoy V.; Platzer, André; Krogh, Bruce: Numerically-aided deductive safety proof for a powertrain control system (2015)
  20. Bak, Stanley; Bogomolov, Sergiy; Johnson, Taylor T.: HYST: a source transformation and translation tool for hybrid automaton models (2015)

1 2 3 4 5 6 next