More Web Proxy on the site http://driver.im/

Article

Techniques for scaling up analyses based on pre-interpretations

Authors:

John P. Gallagher,

Kim S. Henriksen,

Gourinath BandaAuthors Info & Claims

ICLP'05: Proceedings of the 21st international conference on Logic Programming

Pages 280 - 296

https://doi.org/10.1007/11562931_22

Published: 02 October 2005 Publication History

Abstract

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.

References

[1]

Gallagher, J.P., Boulanger, D., Saǧlam, H.: Practical model-based static analysis for definite logic programs. In Lloyd, J.W., ed.: Proc. of International Logic Programming Symposium, MIT Press (1995) 351-365.

[2]

Gallagher, J.P., Henriksen, K.S.: Abstract domains based on regular types. In Lifschitz, V., Demoen, B., eds.: Proceedings of the International Conference on Logic Programming (ICLP'2004). Volume 3132 of Springer-Verlag Lecture Notes in Computer Science. (2004) 27-42.

[3]

Craig, S., Gallagher, J.P., Leuschel, M., Henriksen, K.S.: Fully automatic binding time analysis for Prolog. In Etalle, S., ed.: Pre-Proceedings, 14th International Workshop on Logic-Based Program Synthesis and Transformation, LOPSTR 2004, Verona, August 2004. (2004) 61-70.

[4]

Lloyd, J.: Foundations of Logic Programming: 2nd Edition. Springer-Verlag (1987).

[5]

Boulanger, D., Bruynooghe, M., Denecker, M.: Abstracting s-semantics using a model-theoretic approach. In Hermenegildo, M., Penjam, J., eds.: Proc. 6th International Symposium on Programming Language Implementation and Logic Programming, PLILP'94. Volume 844 of Springer-Verlag Lecture Notes in Computer Science. (1994) 432-446.

[6]

Boulanger, D., Bruynooghe, M.: A systematic construction of abstract domains. In Le Charlier, B., ed.: Proc. First International Static Analysis Symposium, SAS'94. Volume 864 of Springer-Verlag Lecture Notes in Computer Science. (1994) 61-77.

[7]

Corsini, M.M., Musumbu, K., Rauzy, A., Le Charlier, B.: Efficient bottom-up abstract interpretation of prolog by means of constraint solving over symbolic finite domains. In Bruynooghe, M., Penjam, J., eds.: Programming Language Implementation and Logic Programming, 5th International Symposium, PLILP'93. Volume 714 of Springer-Verlag Lecture Notes in Computer Science. (1994) 75-91.

[8]

Codish, M., Demoen, B.: Analysing logic programs using "Prop"-ositional logic programs and a magic wand. In Miller, D., ed.: Proceedings of the 1993 International Symposium on Logic Programming, Vancouver, MIT Press (1993).

[9]

Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, Los Angeles. (1977) 238-252.

[10]

Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications. http://www.grappa.univ-lille3. fr/tata (1999).

[11]

Ullman, J.: Principles of Knowledge and Database Systems; Volume 1. Computer Science Press (1988).

[12]

Dawson, S., Ramakrishnan, C.R., Warren, D.S.: Practical program analysis using general purpose logic programming systemsa case study. In: Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation. (May 1996) 17-126.

[13]

Whaley, J., Lam, M.S.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In Pugh, W., Chambers, C., eds.: PLDI, ACM (2004) 131-144.

[14]

Whaley, J., Unkel, C., Lam, M.S.: A bdd-based deductive database for program analysis (2004) http://bddbddb.sourceforge.net/.

[15]

Lind-Nielsen, J.: BuDDy, a binary decision diagram package (2004) http://sourceforge.net/projects/buddy.

[16]

Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (2000).

[17]

Howe, J.M., King, A.: Positive Boolean Functions as Multiheaded Clauses. In Codognet, P., ed.: International Conference on Logic Programming. Volume 2237 of LNCS. (2001) 120-134.

[18]

Gallagher, J.P., Puebla, G.: Abstract Interpretation over Non-Deterministic Finite Tree Automata for Set-Based Analysis of Logic Programs. In: Fourth International Symposium on Practical Aspects of Declarative Languages (PADL'02). LNCS (2002).

[19]

Genet, T., Tong, V.V.T.: Reachability analysis of term rewriting systems with Timbuk. In Nieuwenhuis, R., Voronkov, A., eds.: LPAR. Volume 2250 of Lecture Notes in Computer Science., Springer (2001) 695-706.

[20]

Marriott, K., Søndergaard, H.: Bottom-up abstract interpretation of logic programs. In: Proceedings of the Fifth International Conference and Symposium on Logic Programming, Washington. (1988).

[21]

Schachte, P.: Precise and Efficient Static Analysis of Logic Programs. PhD thesis, Dept. of Computer Science, The University of Melbourne, Australia (1999).

[22]

Banda, G.: Scalable real-time kernel for small embedded systems. Master's thesis, Southern Univ. of Denmark, Sønderborg (2003).

[23]

Charatonik, W., Podelski, A.: Set-based analysis of reactive infinite-state systems. In Steffen, B., ed.: Proc. of TACAS'98, Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS '98. Volume 1384 of Springer-Verlag Lecture Notes in Computer Science. (1998).

[24]

Goubault-Larrecq, J.: A method for automatic cryptographic protocol verification. In Rolim, J.D.P., ed.: 15 IPDPS 2000 Workshops, Cancun, Mexico, May 1-5, 2000, Proceedings. Volume 1800 of Springer-Verlag Lecture Notes in Computer Science., Springer (2000) 977-984.

[25]

Monniaux, D.: Abstracting cryptographic protocols with tree automata. Sci. Comput. Program. 47(2-3) (2003) 177-202.

[26]

Comon, H., Kozen, D., Seidl, H., Vardi, M.: Applications of Tree Automata in Rewriting, Logic and Programming. Schloß Dagstuhl Seminar 9743, http://www.informatik.uni-trier.de/~seidl/Trees.html (October 20- 24, 1997).

[27]

Heintze, N.: Using bottom-up tree automaton to solve definite set constraints. Unpublished. Presentation at Schloß Dagstuhl Seminar 9743, http://www.informatik.uni-trier.de/~seidl/Trees.html (1997).

[28]

Börstler, J., Möncke, U., Wilhelm, R.: Table compression for tree automata. ACM Trans. Program. Lang. Syst. 13 (1991) 295-314.

[29]

Iwaihara, M., Inoue, Y.: Bottom-up evaluation of logic programs using binary decision diagrams. In Yu, P.S., Chen, A.L.P., eds.: ICDE, IEEE Computer Society (1995) 467-474.

Cited By

Nguyen MDe schreye DGiesl JSchneider-kamp P(2011)PolytoolTheory and Practice of Logic Programming10.1017/S147106841000002511:1(33-63)Online publication date: 1-Jan-2011
https://dl.acm.org/doi/10.1017/S1471068410000025
Gallagher J(2011)Analysis of logic programs using regular tree languagesProceedings of the 21st international conference on Logic-Based Program Synthesis and Transformation10.1007/978-3-642-32211-2_1(1-3)Online publication date: 18-Jul-2011
https://dl.acm.org/doi/10.1007/978-3-642-32211-2_1
Schäfer Mde Moor O(2010)Type inference for datalog with complex type hierarchiesACM SIGPLAN Notices10.1145/1707801.170631745:1(145-156)Online publication date: 17-Jan-2010
https://dl.acm.org/doi/10.1145/1707801.1706317
Show More Cited By

Techniques for scaling up analyses based on pre-interpretations
1. Theory of computation
  1. Logic

Recommendations

Compare less, defer more: scaling value-contexts based whole-program heap analyses
CC 2019: Proceedings of the 28th International Conference on Compiler Construction

The precision of heap analyses determines the precision of several associated optimizations, and has been a prominent area in compiler research. It has been shown that context-sensitive heap analyses are more precise than the insensitive ones, but their ...
Practical escape analyses: how good are they?
VEE '07: Proceedings of the 3rd international conference on Virtual execution environments

A key analysis developed for the compilation of parallel programs is thread escape analysis (hereafter referred to as escape analysis), which determines what objects are accessed in more than one thread, and which references within a program are ...
Parallelizing top-down interprocedural analyses
PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation

Modularity is a central theme in any scalable program analysis. The core idea in a modular analysis is to build summaries at procedure boundaries, and use the summary of a procedure to analyze the effect of calling it at its calling context. There are ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ICLP'05: Proceedings of the 21st international conference on Logic Programming

October 2005

453 pages

ISBN:354029208X

Editors:
Maurizio Gabbrielli
Dipartimento di Scienze dell'Informazione, Universitá di Bologna, Italy
,
Gopal Gupta
Department of Computer Science, University of Texas at Dallas, Richardson, TX, Italy

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 02 October 2005

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 11 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Nguyen MDe schreye DGiesl JSchneider-kamp P(2011)PolytoolTheory and Practice of Logic Programming10.1017/S147106841000002511:1(33-63)Online publication date: 1-Jan-2011
https://dl.acm.org/doi/10.1017/S1471068410000025
Gallagher J(2011)Analysis of logic programs using regular tree languagesProceedings of the 21st international conference on Logic-Based Program Synthesis and Transformation10.1007/978-3-642-32211-2_1(1-3)Online publication date: 18-Jul-2011
https://dl.acm.org/doi/10.1007/978-3-642-32211-2_1
Schäfer Mde Moor O(2010)Type inference for datalog with complex type hierarchiesACM SIGPLAN Notices10.1145/1707801.170631745:1(145-156)Online publication date: 17-Jan-2010
https://dl.acm.org/doi/10.1145/1707801.1706317
Schäfer Mde Moor OHermenegildo MPalsberg J(2010)Type inference for datalog with complex type hierarchiesProceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1706299.1706317(145-156)Online publication date: 17-Jan-2010
https://dl.acm.org/doi/10.1145/1706299.1706317
de Moor OSereni DAvgustinov PVerbaere MKolaitis PLenzerini M(2008)Type inference for datalog and its application to query optimisationProceedings of the twenty-seventh ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems10.1145/1376916.1376957(291-300)Online publication date: 9-Jun-2008
https://dl.acm.org/doi/10.1145/1376916.1376957
Kettle NKing AStrzemecki T(2006)Widening ROBDDs with prime implicantsProceedings of the 12th international conference on Tools and Algorithms for the Construction and Analysis of Systems10.1007/11691372_7(105-119)Online publication date: 25-Mar-2006
https://dl.acm.org/doi/10.1007/11691372_7
Gallagher JPuebla GAlbert E(2005)Converting one type-based abstract domain to anotherProceedings of the 15th international conference on Logic Based Program Synthesis and Transformation10.1007/11680093_10(147-162)Online publication date: 7-Sep-2005
https://dl.acm.org/doi/10.1007/11680093_10

View Options

View options

Media

Figures

Other

Tables

View Table of Contents