کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
9655897 | 685206 | 2005 | 19 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Efficient Proof Engines for Bounded Model Checking of Hybrid Systems
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: Efficient Proof Engines for Bounded Model Checking of Hybrid Systems Efficient Proof Engines for Bounded Model Checking of Hybrid Systems](/preview/png/9655897.png)
چکیده انگلیسی
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.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 133, 31 May 2005, Pages 119-137
Journal: Electronic Notes in Theoretical Computer Science - Volume 133, 31 May 2005, Pages 119-137
نویسندگان
Martin Fränzle, Christian Herde,