Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic

  • Hiroaki Shimizu
  • Kiyoharu Hamaguchi
  • Toshinobu Kashiwabara
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5311)


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.


Quantifier-free first order logic state exploration term-height reduction model checking 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    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)Google Scholar
  6. 6.
  7. 7.
    Armando, A., Benerecetti, M., Carotenuto, D., Mantovani, J., Spica, P.: The Eureka Tool for Software Model Checking. In: 22nd IEEE/ACM ASE Conference (2007)Google Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    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)Google Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)CrossRefzbMATHGoogle Scholar
  13. 13.
    Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)CrossRefGoogle Scholar
  14. 14.
    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)Google Scholar
  15. 15.
    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)CrossRefGoogle Scholar
  16. 16.
    Yices: An SMT Solver,
  17. 17.

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Hiroaki Shimizu
    • 1
  • Kiyoharu Hamaguchi
    • 1
  • Toshinobu Kashiwabara
    • 1
  1. 1.Graduate School of Information Science & TechnologyOsaka UniversityOsakaJapan

Personalised recommendations