HySAT: An efficient proof engine for bounded model checking of hybrid systems n this paper we present HySAT, a bounded model checker for linear hybrid systems, incorporating a tight integration of a DPLL-based pseudo-Boolean SAT solver and a linear programming routine as core engine. In contrast to related tools like MathSAT, ICS, or CVC, our tool exploits the various optimizations that arise naturally in the bounded model checking context, e.g. isomorphic replication of learned conflict clauses or tailored decision strategies, and extends them to the hybrid domain. We demonstrate that those optimizations are crucial to the performance of the tool.

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

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

1 2 next

  1. Cattaruzza, Dario; Abate, Alessandro; Schrammel, Peter; Kroening, Daniel: Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration (2021)
  2. Fahrenberg, Uli; Legay, Axel; Quaas, Karin: Computing branching distances with quantitative games (2020)
  3. 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)
  4. Bak, Stanley; Bogomolov, Sergiy; Althoff, Matthias: Time-triggered conversion of guards for reachability analysis of hybrid automata (2017)
  5. Rebiha, Rachid; Moura, Arnaldo V.; Matringe, Nadir: Generating invariants for non-linear hybrid systems (2015)
  6. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano: Quantifier-free encoding of invariants for hybrid systems (2014)
  7. Xie, Dingbao; Bu, Lei; Zhao, Jianhua; Li, Xuandong: SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata (2014)
  8. Yan, Chao; Greenstreet, Mark R.; Yang, Suwen: Verifying global start-up for a Möbius ring-oscillator (2014)
  9. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano: SMT-based scenario verification for hybrid systems (2013)
  10. Hahn, Ernst Moritz; Hartmanns, Arnd; Hermanns, Holger; Katoen, Joost-Pieter: A compositional modelling and analysis framework for stochastic hybrid systems (2013)
  11. Asplund, Mikael; Manzoor, Atif; Bouroche, Mélanie; Clarke, Siobhàn; Cahill, Vinny: A formal approach to autonomous vehicle coordination (2012) ioport
  12. Badban, Bahareh; Lange, Martin: Exact incremental analysis of timed automata with an SMT-solver (2011)
  13. Schneider, Sven; Nestmann, Uwe: Rigorous discretization of hybrid systems using process calculi (2011)
  14. Teige, Tino; Eggers, Andreas; Fränzle, Martin: Constraint-based analysis of concurrent probabilistic hybrid systems: an application to networked automation systems (2011)
  15. Akbarpour, Behzad; Paulson, Lawrence Charles: MetiTarski: An automatic theorem prover for real-valued special functions (2010)
  16. Fränzle, Martin; Teige, Tino; Eggers, Andreas: Engineering constraint solvers for automatic analysis of probabilistic hybrid automata (2010)
  17. Eggers, Andreas; Kalinnik, Natalia; Kupferschmid, Stefan; Teige, Tino: Challenges in constraint-based analysis of hybrid systems (2009)
  18. Ratschan, Stefan; Smaus, Jan-Georg: Finding errors of hybrid systems by optimising an abstraction-based quality estimate (2009)
  19. Eggers, Andreas; Fränzle, Martin; Herde, Christian: SAT modulo ODE: A direct SAT approach to hybrid systems (2008)
  20. Fränzle, Martin; Hermanns, Holger; Teige, Tino: Stochastic satisfiability modulo theory: A novel technique for the analysis of probabilistic hybrid systems (2008)

1 2 next