Over-approximating Descendants by Synchronized Tree Languages

Authors Yohan Boichut, Jacques Chabin, Pierre Réty



PDF
Thumbnail PDF

File

LIPIcs.RTA.2013.128.pdf
  • Filesize: 0.51 MB
  • 15 pages

Document Identifiers

Author Details

Yohan Boichut
Jacques Chabin
Pierre Réty

Cite AsGet BibTex

Yohan Boichut, Jacques Chabin, and Pierre Réty. Over-approximating Descendants by Synchronized Tree Languages. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 128-142, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
https://doi.org/10.4230/LIPIcs.RTA.2013.128

Abstract

Over-approximating the descendants (successors) of a initial set of terms by a rewrite system is used in verification. The success of such verification methods depends on the quality of the approximation. To get better approximations, we are going to use non-regular languages. We present a procedure that always terminates and that computes over-approximation of descendants, using synchronized tree-(tuple) languages expressed by logic programs.
Keywords
  • rewriting systems
  • non-regular approximations
  • logic programming
  • tree languages
  • descendants

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail