Most symbolic model checkers are based on either Binary Decision Diagrams (BDDs), which may grow exponentially large, or Satisfiability (SAT) solvers, whose time requirements rapidly increase with the sequential depth of the circuit. We investigate the integration of BDD-based methods with SAT to speed up the verification of safety properties of the form G f, where f is either prepositional or contains only the next-time temporal operator X. We use BDD-based reachability analysis to find lower bounds on the reachable states and the states that reach the bad states. Then, we use these lower bounds to shorten the counterexample or reduce the depth of the induction step (termination depth). We present experimental results that compare our method to a pure BDD-based method and a pure SAT-based method. Our method can prove properties that are hard for both the BDD-based and the SAT-based methods. © Springer-Verlag 2001.
CITATION STYLE
Awedh, M., & Somenzi, F. (2004). Increasing the robustness of bounded model checking by computing lower bounds on the reachable states. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3312, 230–244. https://doi.org/10.1007/978-3-540-30494-4_17
Mendeley helps you to discover research relevant for your work.