PHAVer

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

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

1 2 3 4 5 next

  1. Colvin, Robert J.: Modelling and analysing neural networks using a hybrid process algebra (2016)
  2. Papadopoulos, Alessandro Vittorio; Prandini, Maria: Model reduction of switched affine systems (2016)
  3. Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano: HRELTL: a temporal logic for hybrid systems (2015)
  4. Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh: Hybrid automata-based CEGAR for rectangular hybrid systems (2015)
  5. Amato, Gianluca; Scozzari, Francesca; Zaffanella, Enea: Efficient constraint/generator removal from double description of polyhedra (2014)
  6. Minopoli, Stefano; Frehse, Goran: Non-convex invariants and urgency conditions on linear hybrid automata (2014)
  7. Mitsch, Stefan; Passmore, Grant Olney; Platzer, André: Collaborative verification-driven engineering of hybrid systems (2014)
  8. Xie, Dingbao; Bu, Lei; Zhao, Jianhua; Li, Xuandong: SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata (2014)
  9. Yan, Chao; Greenstreet, Mark R.; Yang, Suwen: Verifying global start-up for a Möbius ring-oscillator (2014)
  10. Benerecetti, Massimo; Faella, Marco; Minopoli, Stefano: Automatic synthesis of switching controllers for linear hybrid systems: safety control (2013)
  11. Buntins, Matthias; Schicke, Jens-W.; Eggert, Frank; Goltz, Ursula: Hybrid automata as a modelling approach in the behavioural sciences (2013)
  12. Hahn, Ernst Moritz; Hartmanns, Arnd; Hermanns, Holger; Katoen, Joost-Pieter: A compositional modelling and analysis framework for stochastic hybrid systems (2013)
  13. Hänsch, Paul; Diab, Hilal; Makhlouf, Ibtissem Ben; Kowalewski, Stefan: Reachability analysis of linear systems with stepwise constant inputs (2013)
  14. Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh: Hybrid automata-based CEGAR for rectangular hybrid systems (2013)
  15. 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)
  16. Hansen, Hallstein Asheim; Schneider, Gerardo; Steffen, Martin: Reachability analysis of non-linear planar autonomous systems (2012)
  17. Platzer, André: The structure of differential invariants and differential cut elimination (2012)
  18. Zhang, Lijun; She, Zhikun; Ratschan, Stefan; Hermanns, Holger; Hahn, Ernst Moritz: Safety verification for probabilistic hybrid systems (2012)
  19. Braman, Julia M.B.; Murray, Richard M.: Bisimulation conversion and verification procedure for goal-based control systems (2011)
  20. Brihaye, Thomas; Doyen, Laurent; Geeraerts, Gilles; Ouaknine, Joël; Raskin, Jean-François; Worrell, James: On reachability for hybrid automata over bounded time (2011)

1 2 3 4 5 next