Abstract
In order to verify larger and more complicated systems with model checking, it is necessary to apply some abstraction techniques. Using a subset of first-order logic, called EUF, is one of them. The EUF model checking problem is, however, generally undecidable. In this paper, we introduce a technique called term-height reduction, to guarantee the termination of state enumeration in EUF model checking. This technique generates an over-approximate set of states including all the reachable states. By checking a designated invariant property, we can guarantee whether the invariant property always holds for the design, when verification succeeds. We apply our algorithm to a simple C program and a DSP design and show the experimental results.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Burch, J.R., Dill, D.L.: Automated verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)
Hamaguchi, K., Urushihara, H., Kashiwabara, T.: Symbolic Checking of Signal-Transition Consistency for Verifying High-Level Designs. In: Hunt Jr., W.A., Johnson, S.D. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 455–469. Springer, Heidelberg (2000)
Hojati, R., Isles, A., Kirkpatrick, D., Brayton, R.K.: Verification using uninterpreted functions and finite instantiations. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 218–232. Springer, Heidelberg (1996)
Isles, A.J., Hojati, R., Brayton, R.K.: Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memory. In: 10th International Conference on Computer Aided Verification, pp. 256–267 (1998)
Armando, A., Benerecetti, M., Carotenuto, D., Mantovani, J., Spica, P.: The Eureka Tool for Software Model Checking. In: 22nd IEEE/ACM ASE Conference (2007)
Corella, F., Zhou, Z., Song, X., Langevin, M., Cerny, E.: Multiway Decision Graphs for Automated Hardware Verification. Formal Methods in System Design, vol. 10(1), pp. 7–46 (1997)
Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Convergence Testing in Term-Level Bounded Model Checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 348–362. Springer, Heidelberg (2003)
Kozawa, H., Hamaguchi, K., Kashiwabara, T.: Satisfiability Checking for Logic with Equality and Uninterpreted Functions under Equivalence Constraints. In: IEICE Trans. on Fundamentals of Electronics, Communications and Computer Sciences, pp. 2778–2789 (2007)
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)
Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)
Clarke, E.M., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Proceedings of Tools and Algorithms for the Analysis and Construction of Systems, pp. 168–176 (2004)
Bryant, R.E., German, S., Velev, M.N.: Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 78–92. Springer, Heidelberg (2002)
Yices: An SMT Solver, http://yices.csl.sri.com/
OPENCORES.ORG, http://www.opencores.org/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shimizu, H., Hamaguchi, K., Kashiwabara, T. (2008). Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic. In: Cha, S.(., Choi, JY., Kim, M., Lee, I., Viswanathan, M. (eds) Automated Technology for Verification and Analysis. ATVA 2008. Lecture Notes in Computer Science, vol 5311. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88387-6_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-88387-6_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88386-9
Online ISBN: 978-3-540-88387-6
eBook Packages: Computer ScienceComputer Science (R0)