Sciweavers

Share
FMCAD
2004
Springer

Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States

9 years 3 months ago
Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States
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 propositional or contains only the next-time temporal operator X. We use BDDbased 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.
Mohammad Awedh, Fabio Somenzi
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where FMCAD
Authors Mohammad Awedh, Fabio Somenzi
Comments (0)
books