Efficient Proof Engines for Bounded Model Checking of Hybrid Systems

Abstract

In this paper we present HySAT, a bounded model checker for lin-ear hybrid systems, incorporating a tight integration of a DPLL–based pseudo–Boolean SAT solver and a linear programming routine as core en-gine. In contrast to related tools like MathSAT, ICS, or CVC, our tool ex-ploits 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.