Paper Info
Title
Efficient Proof Engines for Bounded Model Checking of Hybrid Systems
Abstract
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.
Year
DOI
Venue
2005
10.1016/j.entcs.2004.08.061
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
satisfiability,various optimizations,related tool,efficient proof engines,conflict clause,decision procedures,hybrid domain,linear programming routine,linear hybrid system,hybrid systems,bounded model checking,dpll-based pseudo-boolean,infinite-state systems,verification,bounded model checking context,sat solver,new bounded model checker,hybrid system,linear program
Discrete mathematics,Model checking,Computer science,Satisfiability,Boolean satisfiability problem,Theoretical computer science,Isomorphism,DPLL algorithm,Linear programming,Hybrid system,Bounded function
Journal
Volume
ISSN
Citations 
133,
Electronic Notes in Theoretical Computer Science
24
PageRank 
References 
Authors
1.45
24
2
Name
Order
Citations
PageRank
Martin Fränzle178661.58
Christian Herde233815.19