Loading...
Please wait, while we are loading the content...
Similar Documents
Space-Efficient Bounded Model Checking Author names
| Content Provider | Semantic Scholar |
|---|---|
| Copyright Year | 2004 |
| Abstract | Current algorithms for bounded model checking use SAT methods for checking satisfiability of Boolean formulae. Methods based on the validity of Quantified Boolean Formulae (QBF) allow an exponentially more succinct representation of formulae to be checked, because no “unrolling” of the transition relation is required. These methods have not been widely used, because of the lack of an efficient decision procedure for QBF. In this paper we present an algorithm for bounded model checking that uses as succinct representation of formulae as possible with QBF-based techniques. We also provide a comparison of our technique with SAT-based and QBF-based ones, using a few available solvers, on real-life industrial benchmarks. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.tau.ac.il/~nachumd/papers/SpaceEfficientBoundedModelChecking1.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
