HySAT:: An efficient proof engine for bounded model checking of hybrid systems
HySAT:: An efficient proof engine for bounded model checking of hybrid systems
复制标题
DOI：
10.1007/s10703-006-0031-0
复制
发表时间：
2007-06-01
影响因子：
0.8
通讯作者：
Herde, Christian
中科院分区：
文献类型：
--
作者：
Fraenzle, Martin;Herde, Christian
在本文中，我们提出了HySAT，有界模型检查线性混合动力系统，结合紧密集成的DPLL为基础的伪布尔SAT求解器和线性规划例程作为核心引擎。与MathSAT，ICS或CVC等相关工具相比，我们的工具利用了在有界模型检查上下文中自然产生的各种优化，例如学习冲突子句或定制决策策略的同构复制，并将其扩展到混合域。我们证明，这些优化是至关重要的工具的性能。
In 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.