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

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

  1. Rebiha, Rachid; Moura, Arnaldo V.; Matringe, Nadir: Generating invariants for non-linear hybrid systems (2015)
  2. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano: Quantifier-free encoding of invariants for hybrid systems (2014)
  3. Xie, Dingbao; Bu, Lei; Zhao, Jianhua; Li, Xuandong: SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata (2014)
  4. Yan, Chao; Greenstreet, Mark R.; Yang, Suwen: Verifying global start-up for a Möbius ring-oscillator (2014)
  5. Cimatti, Alessandro; Mover, Sergio; Tonetta, Stefano: SMT-based scenario verification for hybrid systems (2013)
  6. Hahn, Ernst Moritz; Hartmanns, Arnd; Hermanns, Holger; Katoen, Joost-Pieter: A compositional modelling and analysis framework for stochastic hybrid systems (2013)
  7. Asplund, Mikael; Manzoor, Atif; Bouroche, Mélanie; Clarke, Siobhàn; Cahill, Vinny: A formal approach to autonomous vehicle coordination (2012) ioport
  8. Teige, Tino; Eggers, Andreas; Fränzle, Martin: Constraint-based analysis of concurrent probabilistic hybrid systems: an application to networked automation systems (2011)
  9. Akbarpour, Behzad; Paulson, Lawrence Charles: MetiTarski: An automatic theorem prover for real-valued special functions (2010)
  10. Fränzle, Martin; Teige, Tino; Eggers, Andreas: Engineering constraint solvers for automatic analysis of probabilistic hybrid automata (2010)
  11. Eggers, Andreas; Kalinnik, Natalia; Kupferschmid, Stefan; Teige, Tino: Challenges in constraint-based analysis of hybrid systems (2009)
  12. Ratschan, Stefan; Smaus, Jan-Georg: Finding errors of hybrid systems by optimising an abstraction-based quality estimate (2009)
  13. Eggers, Andreas; Fränzle, Martin; Herde, Christian: SAT modulo ODE: A direct SAT approach to hybrid systems (2008)
  14. Fränzle, Martin; Hermanns, Holger; Teige, Tino: Stochastic satisfiability modulo theory: A novel technique for the analysis of probabilistic hybrid systems (2008)
  15. Teige, Tino; Fränzle, Martin: Stochastic satisfiability modulo theories for non-linear arithmetic (2008)
  16. Damm, Werner; Disch, Stefan; Hungar, Hardi; Jacobs, Swen; Pang, Jun; Pigorsch, Florian; Scholl, Christoph; Waldmann, Uwe; Wirtz, Boris: Exact state set representations in the verification of linear hybrid systems with large discrete state space (2007)
  17. Damm, Werner; Mikschl, Alfred; Oehlerking, Jens; Olderog, Ernst-Rüdiger; Pang, Jun; Platzer, André; Segelken, Marc; Wirtz, Boris: Automating verification of cooperation, control, and design in traffic applications (2007)
  18. Fränzle, Martin; Herde, Christian: HySAT: An efficient proof engine for bounded model checking of hybrid systems (2007)
  19. Smaus, Jan-Georg: On Boolean functions encodable as a single linear pseudo-Boolean constraint (2007)
  20. Fränzle, Martin; Herde, Christian; Teige, Tino; Ratschan, Stefan; Schubert, Tobias: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure (2006)