Abstract
Symbolic model checking is a very successful formal verification technique, classically based on Binary Decision Diagrams (BDDs). Recently, propositional satisfiability (SAT) techniques have been proposed as a computational basis for symbolic model checking, and proved to be an effective alternative to BDD-based techniques. In this paper we show how BDD-based and SAT-based techniques have been effectively integrated within the NuSMV symbolic model checker.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Parosh Aziz Abdulla, Per Bjesse, and Niklas Eén. Symbolic reachability analysis based on SAT-solvers. In Susanne Graf and Michael Schwartzbach, eds., Proc. Tools and Algorithms for the Construction and Analysis of Systems TACAS, Berlin, Germany, volume 1785 of LNCS. Springer-Verlag, 2000.
S. Berezin, S. Campos, and E. M. Clarke. Compositional reasoning in model checking. In Proc. COMPOS, 1997.
A. Biere, A. Cimatti, E. Clarke, M. Fujita, and Y. Zhu. Symbolic Model Checking Using SAT Procedures instead of BDDs. In Proc. 36th Conference on Design Automation, 1999.
A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proceedings of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’ 99), 1999.
A. Borälv. A Fully Automated Approach for Proving Safety Properties in Interlocking Software Using Automatic Theorem-Proving. In S. Gnesi and D. Latella, eds., Proceedings of the Second International ERCIM Workshop on Formal Methods for Industrial Critical Systems, Pisa, Italy, July 1997.
R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293–318, September 1992.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic Model Checking: 1020 States and Beyond. Information and Computation, 98(2):142–170, June 1992.
A. Cimatti, E.M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new Symbolic Model Verifier. In N. Halbwachs and D. Peled, eds., Proceedings Eleventh Conference on Computer-Aided Verification (CAV’99), number 1633 in Lecture Notes in Computer Science, pages 495–499, Trento, Italy, July 1999. Springer-Verlag.
E. Clarke, O. Grumberg, and K. Hamaguchi. Another Look at LTL Model Checking. Formal Methods in System Design, 10(1):57–71, February 1997.
E. Clarke and X. Zhao. Word Level Symbolic Model Checking: A New Approach for Verifying Arithmetic Circuits. Technical Report CMU-CS-95-161, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213-3891, USA, May 1995.
E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time tem poral logic. In Logic of Programs: Workshop. Springer Verlag, May 1981. Lecture Notes in Computer Science No. 131.
Fady Copty, Limor Fix, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella, and Moshe Vardi. Benefits of bounded model checking at an industrial setting. In Proceedings of CAV 2001, pages 436–453, 2001.
Ranan Fraer, Gila Kamhi, Barukh Ziv, Moshe Y. Vardi, and Limor Fix. Prioritized traversal: Efficient reachability analysis for verification and falsification. In Proceedings of the 12th International Conference on Computer Aided Verification, pages 389–402. Springer, July 2000.
E. Giunchiglia, A. Massarotto, and R. Sebastiani. Act, and the rest will follow: Exploiting determinism in planning as satisfiability. In Proc. AAAI, 1998.
E. Giunchiglia and R. Sebastiani. Applying the Davis-Putnam procedure to nonclausal formulas. In Evelina Lamma and Paola Mello, eds., Proceedings of AI*IA’99: Advances in Artificial Intelligence, pages 84–94. Springer Verlag, 1999.
Enrico Giunchiglia, Marco Maratea, Armando Tacchella, and Davide Zambonin. Evaluating search heuristics and optimization techniques in propositional satisfiability. In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, eds., Proceedings of IJCAR 2001, volume 2083 of Lecture Notes in Computer Science, pages 347–363. Springer, 2001.
G. J. Holzmann. The model checker Spin. IEEE Trans. on Software Engineering, 23(5):279–295, May 1997. Special issue on Formal Methods in Software Practice.
K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publ., 1993.
Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient sat solver. In Proceedings of the 38th Design Automation Conference, pages 530–535. ACM, 2001.
J.P. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proceedings of the Fifth International Symposium in Programming, 1981.
R. K. Ranjan, A. Aziz, B. Plessier, C. Pixley, and R. K. Brayton. Efficient BDD algorithms for FSM synthesis and verification. In IEEE/ACM Proceedings International Workshop on Logic Synthesis, Lake Tahoe (NV), May 1995.
K. Ravi and F. Somenzi. High-density reachability analysis. In International Conference on Computer Aided Design, pages 154–158, Los Alamitos, Ca., USA, November 1995. IEEE Computer Society Press.
O. Shtrichman. Tuning SAT checkers for bounded model-checking. In Proc. 12th International Computer Aided Verification Conference (CAV), 2000.
F. Somenzi. CUDD: CU Decision Diagram package-release 2.1.2. Department of Electrical and Computer Engineering-University of Colorado at Boulder, April 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cimatti, A., Giunchiglia, E., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A. (2002). Integrating BDD-Based and SAT-Based Symbolic Model Checking. In: Armando, A. (eds) Frontiers of Combining Systems. FroCoS 2002. Lecture Notes in Computer Science(), vol 2309. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45988-X_5
Download citation
DOI: https://doi.org/10.1007/3-540-45988-X_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43381-1
Online ISBN: 978-3-540-45988-0
eBook Packages: Springer Book Archive