Techniques for Scaling Up Analyses Based on Pre-interpretations

John Patrick Gallagher, Kim Steen Henriksen, Gourinath Banda

    Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskning


    Any finite tree automaton (or regular type) can be used to construct an abstract interpretation of a logic program, by first determinising and completing the automaton to get a pre-interpretation of the language of the program. This has been shown to be a flexible and practical approach to building a variety of analyses, both generic (such as mode analysis) and program-specific (with respect to a type describing some particular property of interest). Previous work demonstrated the approach using pre-interpretations over small domains. In this paper we present techniques that allow the method to be applied to more complex pre-interpretations and larger programs. There are two main techniques presented: the first is a novel algorithm for determinising finite tree automata, yielding a compact ``product" form of the transitions of the result automaton, that is often orders of magnitude smaller than an explicit representation of the automaton. Secondly, it is shown how this form (which is a representation of a pre-interpretation) can then be input directly to a BDD-based analyser of Datalog programs. We demonstrate through experiments that much more complex analyses become feasible.
    TitelLogic Programming, 21st International Conference
    RedaktørerM. Gabbrielli, G. Gupta
    Antal sider17
    ISBN (Trykt)ISBN 3-540-29208-X
    StatusUdgivet - 2005
    BegivenhedLogic Programming: 21st International Conference - Sitges, Spanien
    Varighed: 2 okt. 20055 okt. 2005
    Konferencens nummer: 21


    KonferenceLogic Programming: 21st International Conference
    NavnLecture Notes in Computer Science

    Citer dette