Abstract
A method of automatic abstraction is presented that uses proofs of unsatisfiability derived from SAT-based bounded model checking as a guide to choosing an abstraction for unbounded model checking. Unlike earlier methods, this approach is not based on analysis of abstract counterexamples. The performance of this approach on benchmarks derived from microprocessor verification indicates that SAT solvers are quite effective in eliminating logic that is not relevant to a given property. Moreover, benchmark results suggest that when bounded model checking successfully terminates, and the problem is unsatisfiable, the number of state variables in the proof of unsatisfiability tends to be small. In almost all cases tested, when bounded model checking succeeded, unbounded model checking of the resulting abstraction also succeeded.
Chapter PDF
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
F. Balarin and A. Sangiovanni-Vincentelli. An iterative approach to language containment. In Computer Aided Verification (CAV’93), pages 29–40, 1993.
J. Baumgratner, A. Kuehlmann, and J. Abraham. Property checking via structural analysis. In Computer-Aided Verification (CAV 2002), pages 151–165, 2002.
A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In TACAS’99, volume 1579 of LNCS, pages 193–207, 1999.
P. Bjesse, T. Leonard, and A. Mokkedem. Finding bugs in an alpha microprocessor using satisfiability solvers. In Computer Aided Verification (CAV 2001), 2001.
E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification, pages 154–169, 2000.
E. M. Clarke, A. Gupta, J. Kukula, and O. Strichman. SAT based abstraction-refinement using ILP and machine learning techniques. In Computer-Aided Verification (CAV 2002), pages 265–279, 2002.
F. Copty, L. Fix, F. R, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Y. Vardi. Benefits of bounded model checking in an industrial setting. In Computer Aided Verification (CAV 2001), pages 436–453, 2001.
S. German. Personal communication.
S. G. Govindaraju and D. L. Dill. Counterexample-Guided choice of projections in approximate symbolic model checking. In IEEE International Conference on Computer Aided Design (ICCAD 2000), pages 115–119, 2000.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 1–33, Washington, D.C., 1990. IEEE Computer Society Press.
O. Kupferman and M. Y. Vardi. Model checking of safety properties. Formal Methods in System Design, 19(3):291–314, 2001.
R. P. Kurshan. Computer-Aided-Verification of Coordinating Processes. Princeton University Press, 1994.
K. L. McMillan and N. Amla. Automatic abstraction without counterexamples. http://www-cad.eecs.berkeley.edu/~kenmcmil/papers, 2002.
M. W. Moskewicz, C. F. Madigan, Y. Z., L. Z., and S. Malik. Cha.: Engineering an efficient SAT solver. In Design Automation Conference, pages 530–535, 2001.
A. P. O. Lichtenstein. Checking that finite state concurrent programs satisfy their linear specification. In POPL’ 85, pages 97–107, 1985.
J. K. S. S. H. V. Pankaj Chauhan, Ed Clarke and D. Wang. Automated abstraction refinement for model checking large state spaces using sat based conflict analysis. In Formal Methods in Computer Aided Design (FMCAD’02), November 2002.
D. Plaisted and S. Greenbaum. A structure preserving clause form translation. Journal of Symbolic Computation, 2:293–304, 1986.
H. Saïdi and S. Graf. Construction of abstract state graphs with PVS. In O. Grumberg, editor, Computer-Aided Verification, CAV’ 97, volume 1254, pages 72–83, Haifa, Israel, 1997. Springer-Verlag.
J. P. M. Silva and K. A. Sakallah. GRASP-a new search algorithm for satisfiability. In Proceedings of the International Conference on Computer-Aided Design, November 1996, 1996.
R. M. T. A. Henzinger, R. Jhala and G. Sutre. Lazy abstraction. In Principles of Programming Languages (POPL 2002), 2002.
M. Vardi and P. Wolper. An automata-theoretic approach to automatic programverification. In Logic in Computer Science (LICS’ 86), pages 322–331, 1986.
D. Wang, P.-H. Ho, J. Long, J. H. Kukula, Y. Zhu, H.-K. T. Ma, and R. Damiano. Formal property verification by abstraction refinement with formal, simulation and hybrid engines. In Design Automation Conference, pages 35–40, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
McMillan, K.L., Amla, N. (2003). Automatic Abstraction without Counterexamples. In: Garavel, H., Hatcliff, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2003. Lecture Notes in Computer Science, vol 2619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36577-X_2
Download citation
DOI: https://doi.org/10.1007/3-540-36577-X_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00898-9
Online ISBN: 978-3-540-36577-8
eBook Packages: Springer Book Archive