Skip to main content

RuleBase Parallel Edition

Formal Verification

Advanced Algorithms

  1. Improvements to the Classical Model Checking Algorithm
    • Improved simplify/assuming algorithm, based on the work of K. Ravi, K. McMillan, T. Shiple, and F. Somenzi, "Approximation and Decomposition of Binary Decision Diagrams," DAC 35th.

    • Efficient state-space search via partitioning of the state-transition function, based on the work of IBM researchers I. Beer and D. Geist, "Efficient Model Checking by Automated Ordering of Transition-Relation Partitioning," CAV '94.

    • Efficient dynamic BDD variable reordering with user control, based on the work of R. Rudell, "Dynamic Variable Ordering for Binary Decision Diagrams," Proc. IEEE ICCAD, San Jose, CA, November 1993.

  2. New Model Checking Algorithms
    • On-the-fly model checking (produce counter-example as you go without first building the entire state space), based on the work of IBM researchers I. Beer and S. Ben-David and A. Landver, "On-the-Fly Model Checking of RCTL Formulas," CAV '98.

    • Specification-directed reachability analysis, a.k.a. "hints", based on the work of K. Ravi, F. Somenzi, "Hints to Accelerate Symbolic Traversal," Proc. CHARME 2000, Lecture Notes in Computer Science, Springer-Verlag, Vol. 1703 pp. 250-264.

    • High-performance bounded model checking based on methods for satisfiability solving, based on the work of IBM researcher O. Shtrichman, "Tuning SAT Checkers for Bounded Model Checking," CAV '00 and CHARME '01, see also journal version "Accellerating Bounded Model Checking of Safety Properties", FMSD '04 (requires ACM Web Account).

    • New powerful heuristics for SAT checking, based on the work of IBM researchers O. Shacham and E. Zarpas, cf. "Tuning the VSIDS Decision Heuristic for Bounded Model Checking", MTV '03, and "Simple Yet Efficient Improvement of SAT Based Bounded Model Checking", FMCAD '04.

    • Optimized bounded model checker based on BDDs, based on the work of IBM researchers R. Tzoref, M. Matusevich, E. Berger and I. Beer. , "An Optimized Symbolic Bounded Model Checking Engine", CHARME '03.

    • Adaptive directed search algorithm, based on the work of IBM researchers S. Keidar and Y. Rodeh, "Searching for Counter-Examples Adaptively", IWFM 2003.

  3. Agressive Reduction Algorithms
    • Traditional localization reduction, based on the work of B. Kurshan, download tutorial.

    • Adaptive localization reduction, based on the work of IBM researchers S. Barner, D. Geist and A. Gringauze, CAV '02.

  4. Services Provided by the Model Checker
    • Detection and explanation of vacuous formulas, based on the work of IBM researchers I. Beer, S. Ben-David, C. Eisner and Y. Rodeh, "Efficient Detection of Vacuity in ACTL Formulas," CAV '97 and FMSD '02.

    • Back-annotation between counter-examples and their respective formulas.

    • Generation of multiple disjoint counter-examples for failed formulas (paper in preparation).