Blog
About

110
views
0
recommends
+1 Recommend
1 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Conference Proceedings: found
      Is Open Access

      SBMC : Symmetric Bounded Model Checking

      , ,

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

      Verification and Evaluation of Computer and Communication Systems (VECoS 2010)

      1-2 July 2010

      Model Checking, Symmetry reduction, SAT, Boolean Formula, Bounded Model Checking, Formal methods

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          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.

          Related collections

          Most cited references 3

          • Record: found
          • Abstract: not found
          • Conference Proceedings: not found

          The temporal logic of programs

           Amir Pnueli (1977)
            Bookmark
            • Record: found
            • Abstract: not found
            • Book Chapter: not found

            Exploiting symmetry in temporal logic model checking

             E. Clarke,  T. Filkorn,  S. Jha (1993)
              Bookmark
              • Record: found
              • Abstract: not found
              • Book Chapter: not found

              Tuning SAT Checkers for Bounded Model Checking

                Bookmark

                Author and article information

                Contributors
                Conference
                July 2010
                July 2010
                : 1-8
                Affiliations
                LIP2 and Faculty of

                Sciences of Tunis

                Campus Universitaire 2092 - El Manar Tunis

                Tunisia
                LIP2 and Polytechnic

                School of Tunisia

                B.P. 743 - 2078 La Marsa

                Fax : +21671748843

                Tunisia
                Article
                10.14236/ewic/VECOS2010.9
                © Brahim NASRAOUI et al. Published by BCS Learning and Development Ltd. Fourth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2010), Paris, France

                This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

                Fourth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2010)
                VECOS
                4
                Paris, France
                1-2 July 2010
                Electronic Workshops in Computing (eWiC)
                Verification and Evaluation of Computer and Communication Systems (VECoS 2010)
                Product
                Product Information: 1477-9358BCS Learning & Development
                Self URI (journal page): https://ewic.bcs.org/
                Categories
                Electronic Workshops in Computing

                Comments

                Comment on this article