Observational Completeness on Abstract Interpretation

• Autorzy: Amato G. , Scozzari F.
• Języki publikacji: EN

Abstrakty

EN

In the theory of abstract interpretation, a domain is complete when abstract computations are as precise as concrete computations. In addition to the standard notion of completeness, we introduce the concept of observational completeness. A domain is observationally complete for an observable when abstract computations are as precise as concrete computations, if we only look at properties in . We prove that continuity of state-transition functions ensures the existence of the least observationally complete domain and we provide a constructive characterization. We study the relationship between the least observationally complete domain and the complete shell. We provide sufficient conditions under which they coincide, and show several examples where they differ, included a detailed analysis of cellular automata.

Słowa kluczowe

EN

abstract interpretation; completeness; static analysis; cellular automata

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 106, nr 2-4
• Strony: 149--173
• Opis fizyczny: Bibliogr. 21 poz., wykr.

Twórcy

autor

Amato G.

autor

Scozzari F.

• Dipartimento di Scienze, viale Pindaro 42, I-65127 Pescara, Italy,

Bibliografia

• [1] Birkhoff, G.: Lattice Theory, vol. XXV of AMS Colloquium Publications, third edition, American Mathematical Society, 1967.
• [2] Comini, M., Levi, G., Meo, M. C.: A Theory of Observables for Logic Programs, Information and Computation, 169(1), 2001, 23-80, ISSN 0890-5401.
• [3] Cortesi, A., Filé, G.,Winsborough,W.W.: The Quotient of an Abstract Interpretation, Theoretical Computer Science, 202(1-2), July 1998, 163-192, ISSN 0304-3975.
• [4] Cousot, P.: Types as Abstract Interpretations, invited paper, in: POPL '97: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM Press, New York, NY, USA, January 1997, ISBN 0-89791-853-3, 316-331.
• [5] Cousot, P., Cousot, R.: Systematic Design of Program Analysis Frameworks, in: POPL '79: Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, ACM Press, New York, NY, USA, January 1979, 269-282.
• [6] Cousot, P., Cousot, R.: Abstract Interpretation and Applications to Logic Programs, The Journal of Logic Programming, 13(2-3), July 1992, 103-179, ISSN 0743-1066.
• [7] Cousot, P., Cousot, R.: Higher-Order Abstract Interpretation (and Application to Comportment Analysis Generalizing Strictness, Termination, Projection and PER Analysis of Functional Languages), Proceedings of the 1994 International Conference on Computer Languages, IEEE Computer Society Press, Los Alamitos, CA, USA, May 1994, ISBN 0-8186-5640-X, Invited paper.
• [8] Cousot, P., Cousot, R.: Temporal Abstract Interpretation, in: POPL '00: Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM Press, New York, NY, USA, January 2000, ISBN 1-58113-125-9, 12-25.
• [9] Dalla Preda, M., Giacobazzi, R.: Semantic-based Code Obfuscation by Abstract Interpretation, Journal of Computer Security, 17(6), 2009, 855-908, ISSN 0926-227X.
• [10] Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems, ACM Transactions on Programming Languages and Systems, 19(2), 1997, 253-291, ISSN 0164-0925.
• [11] Giacobazzi, R., Mastroeni, I.: Adjoining classified and unclassified information by abstract interpretation, Journal of Computer Security. To appear.
• [12] Giacobazzi, R., Quintarelli, E.: Incompleteness, Counterexamples, and Refinements in Abstract Model-Checking, in: Static Analysis, 8th International Symposium, SAS 2001 Paris, France, July 16-18, 2001 Proceedings (P. Cousot, Ed.), vol. 2126 of Lecture Notes in Computer Science, Springer, Berlin Heidelberg, 2001, ISBN 978-3-540-42314-0, 356-373.
• [13] Giacobazzi, R., Ranzato, F.: Incompleteness of states w.r.t. traces in model checking, Information and Computation, 204(3), 2006, 376-407, ISSN 0890-5401.
• [14] Giacobazzi, R., Ranzato, F., Scozzari, F.: Complete Abstract Interpretations Made Constructive, in: Mathematical Foundations of Computer Science 1998, 23rd International Symposium, MFCS'98 Brno, Czech Republic, August 2428, 1998, Proceedings (L. Brim, J. Gruska, J. Zlatuska, Eds.), vol. 1450 of Lecture Notes in Computer Science, Springer, Berlin Heidelberg, 1998, ISBN 978-3-540-64827-7, 366-377.
• [15] Giacobazzi, R., Ranzato, F., Scozzari, F.: Making Abstract Interpretations Complete, Journal of the ACM, 47(2), 2000, 361-416, ISSN 0004-5411.
• [16] Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract domains condensing, ACM Transactions on Computational Logic, 6(1), 2005, 33-60, ISSN 1529-3785.
• [17] Mycroft, A.: Completeness and predicate-based abstract interpretation, Proceedings of the ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, PEPM'93, ACM Press, New York, NY, USA, 1993, ISBN 0-89791-594-1.
• [18] Ranzato, F., Tapparo, F.: Generalizing strong preservation by abstract interpretation, Journal of Logic and Computation, 17(1), 2007, 157-197, ISSN 1465-363X (online) 0955-792X (print).
• [19] Ranzato, F., Tapparo, F.: Generalizing the Paige-Tarjan algorithm by abstract interpretation, Information and Computation, 206(5), 2008, 620-651, ISSN 0890-5401.
• [20] Schmidt, D. A.: Comparing Completeness Properties of Static Analyses and Their Logics, in: Programming Languages and Systems, 4th Asian Symposium, APLAS 2006, Sydney, Australia, November 8-10, 2006. Proceedings (N. Kobayashi, Ed.), vol. 4279 of Lecture Notes in Computer Science, Springer, Berlin Heidelberg, 2006, ISBN 978-3-540-48937-5, 183-199.
• [21] Scozzari, F.: Abstract domains for sharing analysis by optimal semantics, in: Static Analysis, 7th International Symposium, SAS 2000, Santa Barbara, CA, USA, June 29 - July 1, 2000, Proceedings (J. Palsberg, Ed.), vol. 1824 of Lecture Notes in Computer Science, Springer, Berlin Heidelberg, 2000, ISBN 978-3-540-67668-6, 397-412.