Skip to main content
SpringerLink
Log in

Verification of Data Paths Using Unbounded Integers: Automata Strike Back

  • Conference paper
Hardware and Software, Verification and Testing (HVC 2006)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4383))

Included in the following conference series:

Abstract

We present a decision procedure for quantifier-free Presburger arithmetic that is based on a polynomial time translation of Presburger formulas to alternating finite automata (AFAs). Moreover, our approach leverages the advances in SAT solving by reducing the emptiness problem of AFAs to satisfiability problems of propositional logic. In order to obtain a complete decision procedure, we use an inductive style of reasoning as originally proposed for proving safety properties in bounded model checking. Besides linear arithmetic constraints, our decision procedure can deal with bitvector operations that frequently occur in hardware design. Thus, it is well-suited for the verification of data paths at a high level of abstraction.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Leja, F. (ed.): Sprawozdanie z I Kongresu Matematyków Krajów Słowiańskich, Warszawa, 1929 (Comptes–rendus du I Congrés des Mathématiciens des Pays Slaves, Varsovie 1929), Warszawa, pp. 92–101 (supplement on p. 395) (1929)

    Google Scholar 

  2. Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and verification of out-of-order microprocessors in UCLID. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 142–159. Springer, Heidelberg (2002)

    Google Scholar 

  3. Büchi, J.: Weak second order arithmetic and finite automata. Z. Math. Logik Grundlagen Math. 6, 66–92 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  4. Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and finite automata. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol. 1059, pp. 30–43. Springer, Heidelberg (1996)

    Google Scholar 

  5. Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol. 1785, pp. 1–19. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  6. Klaedtke, F.: On the automata size for Presburger arithmetic. Technical Report 186, Institute of Computer Science at Freiburg University (2003)

    Google Scholar 

  7. Ganesh, V., Berezin, S., Dill, D.L.: Deciding Presburger arithmetic by model checking and comparisons with other methods. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 171–186. Springer, Heidelberg (2002)

    Google Scholar 

  8. Seshia, S.A., Bryant, R.E.: Deciding quantifier-free Presburger formulas using parameterized solution bounds. Logical Methods in Computer Science 1(2:6), 1–26 (2005)

    MathSciNet  Google Scholar 

  9. Boigelot, B.: The Liège automata-based symbolic handler (LASH) (2006), http://www.montefiore.ulg.ac.be/~boigelot/research/lash/

  10. Janicic, P., Green, I., Bundy, A.: A comparison of decision procedures in Presburger arithmetic. Research Paper 872, University of Edinburgh (1997)

    Google Scholar 

  11. Shiple, T.R., Kukula, J.H., Ranjan, R.K.: A comparison of Presburger engines for EFSM reachability. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 280–292. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  12. Schuele, T., Schneider, K.: Symbolic model checking by automata based set representation. In: Ruf, J. (ed.) Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, Tübingen, Germany, GI/ITG/GMM, pp. 229–238. Shaker, Aachen (2002)

    Google Scholar 

  13. Strichman, O.: On solving Presburger and linear arithmetic with SAT. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 160–170. Springer, Heidelberg (2002)

    Google Scholar 

  14. Kroening, D., et al.: Abstraction-based satisfiability solving of Presburger arithmetic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 308–320. Springer, Heidelberg (2004)

    Google Scholar 

  15. Yu, S.: Regular languages. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. 1, pp. 41–110. Springer, Heidelberg (1997)

    Google Scholar 

  16. Fellah, A., Jürgensen, H., Yu, S.: Constructions for alternating finite automata. International Journal of Computer Mathematics 35, 117–132 (1990)

    Article  MATH  Google Scholar 

  17. Fellah, A.: Equations and regular-like expressions for AFA. International Journal of Computer Mathematics 51, 157–172 (1994)

    Article  MATH  Google Scholar 

  18. Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. Journal of the ACM 28(1), 114–133 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  19. Brzozowski, J.A., Leiss, E.: On equations for regular languages, finite automata, and sequential networks. Theoretical Computer Science 10, 19–35 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  20. Leiss, E.: Succinct representation of regular languages by Boolean automata. Theoretical Computer Science 13, 323–330 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  21. Leiss, E.: Succinct representation of regular languages by Boolean automata II. Theoretical Computer Science 38, 133–136 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  22. Huerter, S., et al.: Implementing reversed alternating finite automaton (r-AFA) operations. In: Champarnaud, J.-M., Maurel, D., Ziadi, D. (eds.) WIA 1998. LNCS, vol. 1660, pp. 69–81. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  23. Salomaa, K., Wu, X., Yu, S.: Efficient implementation of regular languages using r-AFA. In: Wood, D., Yu, S. (eds.) WIA 1997. LNCS, vol. 1436, pp. 176–184. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  24. Salomaa, K., Wu, X., Yu, S.: Efficient implementation of regular languages using reversed alternating finite automata. Theoretical Computer Science 231(1), 103–111 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  25. Tuerk, T., Schneider, K.: Relationship between alternating omega-automata and symbolically represented nondeterministic omega-automata. Internal Report 340, Department of Computer Science, University of Kaiserslautern (2005), http://kluedo.ub.uni-kl.de

  26. Bès, A.: A survey of arithmetical definability. Bulletin of the Société Mathématique Belgique, 1–54 (2002)

    Google Scholar 

  27. Bruyere, V., et al.: Logic and p-recognizable sets of integers. Bulletin of the Société Mathématique Belgique 1, 191–238 (1994)

    MathSciNet  MATH  Google Scholar 

  28. von zur Gathen, J., Sieveking, M.: A bound on solutions of linear integer equalities and inequalities. Proceedings of the American Mathematical Society 72(1), 155–158 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  29. Hardy, G.H., Wright, E.M.: An introduction to the theory of numbers. Oxford University Press, Oxford (1979)

    MATH  Google Scholar 

  30. Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  31. Ranise, S., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2006), http://goedel.cs.uiowa.edu/smtlib

Download references

Author information

Authors and Affiliations

  1. Reactive Systems Group, Department of Computer Science, University of Kaiserslautern, P.O. Box 3049, 67653 Kaiserslautern, Germany

    Tobias Schuele & Klaus Schneider

Authors
  1. Tobias Schuele
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Klaus Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Eyal Bin Avi Ziv Shmuel Ur

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer Berlin Heidelberg

About this paper

Cite this paper

Schuele, T., Schneider, K. (2007). Verification of Data Paths Using Unbounded Integers: Automata Strike Back. In: Bin, E., Ziv, A., Ur, S. (eds) Hardware and Software, Verification and Testing. HVC 2006. Lecture Notes in Computer Science, vol 4383. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70889-6_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-70889-6_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-70888-9

  • Online ISBN: 978-3-540-70889-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation