Efficient Proof Engines for Bounded Model Checking of Hybrid Systems

Martin Fränzle, Christian Herde

    Research output: Contribution to journalJournal articleResearchpeer-review

    153 Downloads (Pure)


    In this paper we present HySat, a new 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 all of 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.
    Original languageEnglish
    JournalElectronic Notes in Theoretical Computer Science
    Pages (from-to)119-137
    Publication statusPublished - 2005


    • satisfiability
    • hybrid systems
    • infinite-state systems
    • verification
    • bounded model checking
    • decision procedures


    Dive into the research topics of 'Efficient Proof Engines for Bounded Model Checking of Hybrid Systems'. Together they form a unique fingerprint.

    Cite this