In this chapter, we present a decision procedure which is tailored to fit the needs of BMC of infinite-state systems with piecewise linear variable updates, e.g. of linear hybrid automata, as introduced in chapter 2. Our tool, we name it HySAT-1, tightly integrates a DPLL style SAT solver with a linear programming routine, combining the virtues of both methods: Linear programming adds the capability of solving large conjunctive systems of linear inequalities over the reals, whereas the SAT solver accounts for fast Boolean search and efficient handling of disjunctions. Building on the work presented in chapter 3, we use our pseudo-Boolean solver GOBLIN as SAT engine in HySAT-1.


Linear Constraint Hybrid Automaton Bound Model Check Linear Programming Solver Linear Arithmetic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Vieweg+Teubner Verlag | Springer Fachmedien Wiesbaden GmbH 2011

Authors and Affiliations

  • Christian Herde

There are no affiliations available

Personalised recommendations