Abstract
The introduction of symbolic model checking using Binary Decision Diagrams (BDDs) has led to a substantial extension of the class of systems that can be algorithmically verified. Although BDDs have played a crucial role in this success, they have some well-known drawbacks, such as requiring an externally supplied variable ordering and causing space blowups in certain applications. In a parallel development, SAT-solving procedures, such as Stålmarck’s method or the Davis-Putnam procedure, have been used successfully in verifying very large industrial systems. These efforts have recently attracted the attention of the model checking community resulting in the notion of bounded model checking. In this paper, we show how to adapt standard algorithms for symbolic reachability analysis to work with SAT-solvers. The key element of our contribution is the combination of an algorithm that removes quantifiers over propositional variables and a simple representation that allows reuse of subformulas. The result will in principle allow many existing BDD-based algorithms to work with SAT-solvers. We show that even with our relatively simple techniques it is possible to verify systems that are known to be hard for BDD-based model checkers.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
H. R. Andersen and H. Hulgaard. Boolean expression diagrams. In Proc. 12th IEEE Int. Symp. on Logic in Computer Science, pages 88–98, 1997. 413, 424
BCC+99._A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Design Automation Conference (DAC’99), 1999. 412
A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. TACAS’ 98, 8th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 1999. 412
J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill. Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142–170, 1992. 411
A. Biere, E. M. Clarke, R. Raimi, and Y. Zhu. Verifying safety properties of a PowerPC[tm] microprocessor using symbolic model checking without BDDs. In Proc. 11th Int. Conf. on Computer Aided Verification, 1999. 412
P. Bjesse. Symbolic model checking with sets of states represented as formulas. Technical Report CS-1999-100, Department of Computer Science, Chalmers technical university, March 1999. 412, 424
A. Borälv. The industrial success of verification tools based on Stålmarck’s method. In Proc. 9th Int. Conf. on Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 7–10, 1997. 412
A. Borälv. Case study: Formal verification of a computerized railway interlocking. Formal Aspects of Computing, 10(4):338–360, 1998. 412
R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers, C-35(8):677–691, Aug. 1986. 411
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Trans. on Programming Languages and Systems, 8(2):244–263, April 1986. 411
N. Eén. Symbolic reachability analysis based on SAT-solvers. Master’s thesis, Dept. of Computer Systems, Uppsala university, 1999. 412, 420
J.F. Groote, S.F.M. van Vlijmen, and J.W.C. Koorn. The safety guaranteeing system at station Hoorn-Kersenboogerd. In COMPASS’95, 1995. 412
H. Hulgaard, P.F. Williams, and H.R. Andersen. Combinational logic-level verification using boolean expression diagrams. In 3rd International Workshop on Applications of the Reed-Muller Expansion in Circuit Design, 1997. 413, 424
K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993. 411
C. Papadimitriou. Computational complexity. Addison-Wesley, 1994. 412
J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In 5th International Symposium on Programming, Turin, volume 137 of Lecture Notes in Computer Science, pages 337–352. Springer Verlag, 1982. 411
G. Stålmarck and M. Säflund. Modelling and verifying systems and software in propositional logic. In SAFECOMP’90, pages 31–36. Pergamon Press, 1990. 412
M. Sheeran and G. Stålmarck. A tutorial on Stålmarck’s method of propositional proof. Formal Methods In System Design, 16(1), 2000. 412
G. Stålmarck. A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula. Swedish Patent No. 467 076 (approved 1992), US patent No. 5 276 897 (1994), European Patent No. 0403 454 (1995). 412
H. Zhang. SATO: an efficient propositional prover. In Proc. Int. Conference om Automated Deduction (CADE’97), volume 1249 of LNAI, pages 272–275. Springer Verlag, 1997. 412
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abdulla, P.A., Bjesse, P., Eén, N. (2000). Symbolic Reachability Analysis Based on SAT-Solvers. In: Graf, S., Schwartzbach, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2000. Lecture Notes in Computer Science, vol 1785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46419-0_28
Download citation
DOI: https://doi.org/10.1007/3-540-46419-0_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67282-1
Online ISBN: 978-3-540-46419-8
eBook Packages: Springer Book Archive