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 83 articles , 1 standard article )

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

1 2 3 4 5 next

  1. Dreossi, Tommaso; Dang, Thao; Piazza, Carla: Reachability computation for polynomial dynamical systems (2017)
  2. Baştuğ, Mert; Petreczky, Mihály; Wisniewski, Rafael; Leth, John: Reachability and observability reduction for linear switched systems with constrained switching (2016)
  3. Colvin, Robert J.: Modelling and analysing neural networks using a hybrid process algebra (2016)
  4. Papadopoulos, Alessandro Vittorio; Prandini, Maria: Model reduction of switched affine systems (2016)
  5. Aréchiga, Nikos; Kapinski, James; Deshmukh, Jyotirmoy V.; Platzer, André; Krogh, Bruce: Numerically-aided deductive safety proof for a powertrain control system (2015)
  6. Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano: HRELTL: a temporal logic for hybrid systems (2015)
  7. Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh: Hybrid automata-based CEGAR for rectangular hybrid systems (2015)
  8. Amato, Gianluca; Scozzari, Francesca; Zaffanella, Enea: Efficient constraint/generator removal from double description of polyhedra (2014)
  9. Minopoli, Stefano; Frehse, Goran: Non-convex invariants and urgency conditions on linear hybrid automata (2014)
  10. Mitsch, Stefan; Passmore, Grant Olney; Platzer, André: Collaborative verification-driven engineering of hybrid systems (2014) ioport
  11. Xie, Dingbao; Bu, Lei; Zhao, Jianhua; Li, Xuandong: SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata (2014)
  12. Yan, Chao; Greenstreet, Mark R.; Yang, Suwen: Verifying global start-up for a Möbius ring-oscillator (2014)
  13. Benerecetti, Massimo; Faella, Marco; Minopoli, Stefano: Automatic synthesis of switching controllers for linear hybrid systems: safety control (2013)
  14. Buntins, Matthias; Schicke, Jens-W.; Eggert, Frank; Goltz, Ursula: Hybrid automata as a modelling approach in the behavioural sciences (2013)
  15. Hahn, Ernst Moritz; Hartmanns, Arnd; Hermanns, Holger; Katoen, Joost-Pieter: A compositional modelling and analysis framework for stochastic hybrid systems (2013)
  16. Hänsch, Paul; Diab, Hilal; Makhlouf, Ibtissem Ben; Kowalewski, Stefan: Reachability analysis of linear systems with stepwise constant inputs (2013)
  17. Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh: Hybrid automata-based CEGAR for rectangular hybrid systems (2013)
  18. Damm, Werner; Dierks, Henning; Disch, Stefan; Hagemann, Willem; Pigorsch, Florian; Scholl, Christoph; Waldmann, Uwe; Wirtz, Boris: Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces (2012)
  19. Hansen, Hallstein Asheim; Schneider, Gerardo; Steffen, Martin: Reachability analysis of non-linear planar autonomous systems (2012)
  20. Platzer, André: The structure of differential invariants and differential cut elimination (2012)

1 2 3 4 5 next