Abstract
Unbounded model checking methods based on Boolean satisfiability (SAT) solvers are proving to be a viable alternative to BDD-based model checking. These methods include, for example, interpolation based and sequential ATPG-based approaches. In this paper, we explore the implications of using abstraction refinement in conjunction with interpolation-based model checking. Based on experiments using a large industrial benchmark set, we conclude that when using interpolation- based model checking, measures must be taken to prevent the overhead of abstraction refinement from dominating runtime. We present two new approaches to this problem. One is a hybrid approach that decides heuristically when to apply abstraction. The other is a very coarse but inexpensive abstraction method based on ideas from ATPG. This approach can produce order-of-magnitude reductions in memory usage, allowing significantly larger designs to be verified.
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
Kurshan, R.P., et al.: An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 254–268. Springer, Heidelberg (2005)
McMillan, K.L., Amla, N.: A Hybrid of Counterexample-Based and Proof-Based Abstraction. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 260–274. Springer, Heidelberg (2004)
Somenzi, F., Awedh, M.: Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 230–244. Springer, Heidelberg (2004)
Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electronic Notes in Theoretical Computer Science 66(2) (2002)
Clarke, E., et al.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol. 1579, Springer, Heidelberg (1999)
Bryant, R.E.: Graph-based algorithms for boolean function manipulations. IEEE Transactions on Computers (1986)
Burch, J.R., et al.: Symbolic model checking: 1020 states and beyond. In: LICS (1990)
Cabodi, G., Nocco, S., Quer, S.: Improving SAT-based bounded model checking by means of bdd-based approximate traversals. In: DATE (2003)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on Logics of Programs (1981)
Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (1990)
Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT-solver. In: DATE (2002)
Gupta, A., et al.: Learning from BDDs in SAT-based bounded model checking. In: DAC (2003)
Gupta, A., et al.: Iterative abstraction using SAT-based BMC with proof analysis. In: ICCAD (2003)
Gupta, A., Strichman, O.: Abstraction Refinement for Bounded Model Checking. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 112–124. Springer, Heidelberg (2005)
Huang, C.Y., et al.: Static property checking using atpg versus bdd techniques. In: ITC (2000)
Iyer, M., Parthasarathy, G., Cheng, K.T.: SATORI- an efficient sequential SAT solver for circuits. In: ICCAD (2003)
Kupferman, O., Vardi, M.: Model checking of safety properties. In: Formal Methods in System Design (2001)
Somenzi, F., Li, B.: Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 227–241. Springer, Heidelberg (2006)
Li, B., Wang, C., Somenzi, F.: Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure. In: STTT (2005)
Marques-Silva, J.: Improvements to the Implementation of Interpolant-Based Model Checking. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 367–370. Springer, Heidelberg (2005)
Marques-Silva, J., Sakallah, K.: GRASP: A search algorithm for propositional satisfiability. IEEETC: IEEE Transactions on Computers 48 (1999)
McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)
McMillan, K.L., Amla, N.: Automatic Abstraction without Counterexamples. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 2–17. Springer, Heidelberg (2003)
Moskewicz, M.W., et al.: Chaff: Engineering an Efficient SAT Solver. In: DAC (2001)
Prasad, M., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. In: STTT (2005)
Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Proc. of the 5th International Symposium on Programming (1982)
Somenzi, F., Ravi, K.: Minimal Assignments for Bounded Model Checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 31–45. Springer, Heidelberg (2004)
Whittemore, J., Kim, J., Sakallah, K.: SATIRE: A new incremental satisfiability engine. In: DAC (2001)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Amla, N., McMillan, K.L. (2007). Combining Abstraction Refinement and SAT-Based Model Checking. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_31
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)