Skip to main content
SpringerLink
Log in

Reachability Analysis of Term Rewriting Systems with Timbuk

  • Conference paper
  • First Online:
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2250))

Abstract

We present Timbuk - a tree automata library - which implements usual operations on tree automata as well as a completion algorithm used to compute an over-approximation of the set of descendants R*(E) for a regular set E and a term rewriting system R, possibly non linear and non terminating. On several examples of term rewriting systems representing programs and systems to verify, we show how to use Timbuk to construct their approximations and then prove unreachability properties of these systems.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

    Google Scholar 

  2. P. Borovanský, C. Kirchner, H. Kirchner, P.-E. Moreau, and M. Vittek. ELAN: A logical framework based on computational systems. In Proc. 1st WRLA, volume 4 of ENTCS, Asilomar (California), 1996.

    Google Scholar 

  3. H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. http://www.grappa.univ-lille3.fr/tata/, 1997.

  4. P. Cousot and R. Cousot. Formal Language, Grammar and Set-Constraint-Based Program Analysis by Abstract Interpretation. In Conference Record of FPCA’95 SIGPLAN/SIGARCH/WG2.8, pages 170–181. ACM Press, 1995.

    Google Scholar 

  5. N. Dershowitz and J.-P. Jouannaud. Handbook of Theoretical Computer Science, volume B, chapter 6: Rewrite Systems, pages 244–320. Elsevier Science Publishers B. V. (North-Holland), 1990. Also as: Research report 478, LRI.

    Google Scholar 

  6. T. Genet. Decidable approximations of sets of descendants and sets of normal forms. In Proc. 9th RTA Conf., Tsukuba (Japan), volume 1379 of LNCS, pages 151–165. Springer-Verlag, 1998.

    Google Scholar 

  7. T. Genet and F. Klay. Rewriting for Cryptographic Protocol Verification. In Proc. 7th CADE Conf., Pittsburgh (Pen., USA), volume 1831 of LNAI. Springer-Verlag, 2000.

    Google Scholar 

  8. T. Genet and V. Viet Triem Tong. Timbuk Documentation. IRISA / Université de Rennes 1, 2001. http://www.irisa.fr/lande/genet/timbuk/.

  9. R. Gilleron and S. Tison. Regular tree languages and rewrite systems. Fundamenta Informaticae, 24:157–175, 1995.

    MATH  MathSciNet  Google Scholar 

  10. F. Jacquemard. Decidable approximations of term rewriting systems. In H. Ganzinger, editor, Proc. 7th RTA Conf., New Brunswick New Jersey, USA, pages 362–376. Springer-Verlag, 1996.

    Google Scholar 

  11. N. Jones. Flow analysis of lazy higher-order functional programs. In S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, pages 103–122. Ellis Horwood, Chichester, England, 1987.

    Google Scholar 

  12. N. Klarlund and A. Møller. MONA Version 1.4 User Manual, January 2001.

    Google Scholar 

  13. X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon. The Objective Caml system release 3.00-Documentation and user’s manual. INRIA, 2000. http://caml.inria.fr/ocaml/htmlman/.

  14. D. Monniaux. Abstracting Cryptographic Protocols with Tree Automata. In Proc. 6th SAS, Venezia (Italy), 1999.

    Google Scholar 

  15. L. Paulson. Proving Properties of Security Protocols by Induction. In 10th Computer Security Foundations Workshop. IEEE Computer Society Press, 1997.

    Google Scholar 

  16. P. Réty. Regular Sets of Descendants for Constructor-based Rewrite Systems. In Proc. 6th LPAR Conf., Tbilisi (Georgia), volume 1705 of LNAI. Springer-Verlag, 1999.

    Google Scholar 

  17. J. Waldmann. RX: an interpreter for Rational Tree Languages, 1998. http://www.informatik.uni-leipzig.de/~joe/rx/.

Download references

Author information

Authors and Affiliations

  1. IRISA, Université de Rennes 1, Campus de Beaulieu, F-35042, Rennes Cedex

    Thomas Genet & Valérie Viet Triem Tong

Authors
  1. Thomas Genet
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Valérie Viet Triem Tong
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Software, Technical University of Catalonia, Jordi Girona 1, 08034, Barcelona, Spain

    Robert Nieuwenhuis

  2. Department of Computer Science, University of Manchester, Kilburn Building, Oxford Road, M13 9PL, Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Genet, T., Tong, V.V.T. (2001). Reachability Analysis of Term Rewriting Systems with Timbuk. In: Nieuwenhuis, R., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2001. Lecture Notes in Computer Science(), vol 2250. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45653-8_48

Download citation

  • DOI: https://doi.org/10.1007/3-540-45653-8_48

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-45653-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation