Abstract
In this paper, we describe a completely automated framework for iterative abstraction refinement that is fully integrated into a formal-verification environment. This environment consists of three basic software tools: Forecast, a BDD-based model checker, Thunder, a SAT-based bounded model checker, and MCE, a technology for multiple-counterexample analysis. In our framework, the initial abstraction is chosen relative to the property under verification. The abstraction is model checked by Forecast; in case of failure, a counterexample is returned. Our framework includes an abstract counterexample analyzer module that applies techniques for bounded model checking to check whether the abstract counterexample holds in the concrete model. If it does, it is extended to a concrete counterexample. This important capability is provided as a separate tool that also addresses one of the major problems of verification by manual abstraction. If the counterexample is spurious, we use a novel refinement heuristic based on MCE to guide the refinement. After the part of the abstract model to be refined is chosen, our refinement algorithm computes a new abstraction that includes as much logic as possible without adding too many new variables, therefore striking a balance between refining the abstraction and keeping its size manageable. We demonstrate the effectiveness of our framework on challenging Intel designs that were not amenable to BDD-based model-checking approaches.
Supported in part by NSF grants CCR-9700061, CCR-9988322, IIS-9908435, IIS-9978135, and EIA-0086264, by BSF grant 9800096, and by a grant from the Intel Corporation.
Chapter PDF
References
R. Armoni, L. Fix, A. Flaisher, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador-Haim, E. Singerman, A. Tiemeyer, M.Y. Vardi, and Y. Zbar. The ForSpec temporal logic: A new temporal property-specification language. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS’02), LNCS. Springer-Verlag, 2002.
F. Balarin and A.L. Sangiovanni-Vincentelli. An iterative approach to language containment. In CAV’93, LNCS, pages 29–40. Springer-Verlag, 1993.
S. Barner, D. Geist, and A. Gringauze. Symbolic localization reduction with reconstruction layering and backtracking. In E. Brinksma and K. G. Larsen, editors, CAV’02, volume 2404 of LNCS, pages 65–77. Springer-Verlag, 2002.
A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for Construction and Analysis of Systems (TACAS’99), volume 1579 of LNCS, pages 193–207. Springer-Verlag, 1999.
P. Biesse, T. Leonard, and A. Mokkedem. Finding bugs in an alpha microprocessors using satisfiability solvers. In CAV’01, volume 2102 of LNCS, pages 454–464. Springer-Verlag, 2001.
B. Bollobas. Graph Theory. Springer-Verlag, 1979.
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.
E. M. Clarke, A. Gupta, J. Kukula, and O. Strichman. SAT based abstraction-refinement using ILP and machine learning techniques. In E. Brinksma and K. G. Larsen, editors, CAV’02, volume 2404 of LNCS, pages 265–279. Springer-Verlag, 2002.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACMTransactions on Programming Languages and Systems, 8(2):244–263, January 1986.
E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV’00, volume 1855 of LNCS, pages 154–169. Springer-Verlag, 2000.
E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512–1542, September 1994.
E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, and M.Y. Vardi. Benefits of bounded model checking at an industrial setting. In CAV’01, volume 2102 of LNCS, pages 436–453. Springer-Verlag, 2001.
F. Copty, A. Irron, O. Weissberg, N.P. Kropp, and G. Kamhi. Efficient debugging in a formal verification environment. In T. Margaria et. al., editor, Correct Hardware Design and Verification Methods (CHARME’01), volume 2144 of LNCS, pages 275–292. Springer-Verlag, 2001.
L.R. Ford and D.R. Fulkerson. Maximal flow through a network. Canadian Journal of Mathematics, 8:399–404, 1956.
R. Fraer, G. Kamhi, B. Ziv, M. Vardi, and L. Fix. Prioritized traversal: efficient reachability analysis for verication and falsification. In CAV’00, volume 1855 of LNCS, pages 389–402. Springer-Verlag, 2000.
G.S. Govindaraju and D.L. Dill. Counterexample-guided choice of projections in approximate symbolic model checking. In ICCAD’00, 2000.
G. Hachtel and F. Somenzi. Synthesis and Verification Algorithms. Kluwer, 1996.
R.H. Hardin, Z. Har’el, and R.P. Kurshan. COSPAN. In CAV’96, volume 1102 of LNCS, pages 423–427. Springer-Verlag, 1996.
R.H. Hardin, R.P. Kurshan, K.L. McMillan, J.A. Reeds, and N.J.A. Sloane. Efficient regression verification. IEE Proc. WODES’96, pages 147–150, 1996.
P.H. Ho, T. Shiple, K. Harer, J.H. Kukula, R. Damiano, V. Bertacco, J. Taylor, and J. Long. Smart simulation using collaborative formal simulation engines. In ICCAD’00, pages 120–126, 2000.
J. Jang, I. Moon, and G. Hachtel. Iterative abstraction-based CTL model checking, 2000.
B. Krishnamurthy. An improved Min-Cut algorithm for partitioning VLSI networks. IEEE Transactions on Computers, 33(5):438–446, 1984.
O. Kupferman and M.Y. Vardi. Model checking of safety properties. Formal Methods in System Design, 19:291–314, 2001.
R.P. Kurshan. Computer AidedVerification of Coordinating Processes. Princeton Univ. Press, 1994.
W. Lee, A. Pardo, J. Jang, G. Hachtel, and F. Somenzi. Tearing based abstraction for CTL model checking. In ICCAD’96, pages 76–81, 1996.
O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proc. 12th ACM Symp. on Principles of Programming Languages, pages 97–107, 1985.
J. Lind-Nielsen and H.R. Andersen. Stepwise CTL model checking of state/event systems. In CAV’99, volume 1633 of LNCS, pages 316–327. Springer-Verlag, 1999.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, January 1992.
K.S. Namjoshi and R.P. Kurshan. Syntactic program transformations for automatic abstraction. n CAV’00, volume 1855 of LNCS, pages 435–449. Springer-Verlag, 2000.
A. Pardo and G. Hachtel. Automatic abstraction techniques for propositional μ-calculus model checking. In CAV’97, volume 1254 of LNCS, pages 12–23. Springer-Verlag, 1997.
A. Pardo and G. Hachtel. Incremental CTL model checking using BDD subsetting. In Design Automation Conference, pages 457–462, 1998.
J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th International Symp. on Programming, volume 137 of LNCS, pages 337–351. Springer-Verlag, 1981.
R. Rudell. DynamicVariable Ordering for Ordered Binary Decision Diagrams. In ICCAD’93, pages 42–47. IEEE Computer Society Press, 1993.
V. Rusu and E. Singerman. On proving safety properties by integrating static analysis, theorem proving and abstraction. In W.R. Cleaveland, editor, TACAS’99, volume 1579 of LNCS, pages 178–192. Springer-Verlag, 1999.
M.Y. Vardi. An automata-theoretic approach to linear temporal logic. In F. Moller and G. Birtwistle, editors, Logics for Concurrency: Structure versus Automata, volume 1043 of LNCS, pages 238–266. Springer-Verlag, 1996.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In 1st Symp. on Logic in Computer Science, pages 332–344, Cambridge, June 1986.
D. Wang, P.H. Ho, J. Long, J.H. Kukula, Y. Zhu, 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
Glusman, M., Kamhi, G., Mador-Haim, S., Fraer, R., Vardi, M.Y. (2003). Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation. 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_13
Download citation
DOI: https://doi.org/10.1007/3-540-36577-X_13
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