Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    SBMC: Symmetric Bounded Model Checking

    Fourth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2010)

    Paris, France, 1 - 2 July 2010


    Brahim Nasraoui, Syrine Ayadi and Riadh Robbana


    This paper deals with systems verification techniques, using Bounded Model Checking (BMC). We present a new approach that combines BMC with symmetry reduction techniques. Our goal is to reduce the number of transition sequences, which can be handled by a SAT solver, used in the resolution of verification problems. In this paper, we generate a reduced model by exploiting the symmetry of the original model,which contains only transition sequences that represent the equivalence classes of the symmetric transition sequences. We consider the construction of a new Boolean formula that manipulates only representative transition sequences. In our technique, we present a method that combines the symmetry reduction technique with BMC for the reduction of the space and time of Model Checking.


    PDF filePDF Version of this Paper (83kb)