publication . Conference object . 2005

Abstract Interpretation-based verification/certification in the ciaoPP system

Puebla Sánchez, Alvaro Germán; Albert Albiol, Elvira; Hermenegildo, Manuel V.;
Open Access English
  • Published: 01 Oct 2005
  • Publisher: Facultad de Informática (UPM)
  • Country: Spain
CiaoPP is the abstract interpretation-based preprocessor of the Ciao multi-paradigm (Constraint) Logic Programming system. It uses modular, incremental abstract interpretation as a fundamental tool to obtain information about programs. In CiaoPP, the semantic approximations thus produced have been applied to perform high- and low-level optimizations during program compilation, including transformations such as múltiple abstract specialization, parallelization, partial evaluation, resource usage control, and program verification. More recently, novel and promising applications of such semantic approximations are being applied in the more general context of progra...
free text keywords: Informática
Related Organizations
Download from
Archivo Digital UPM
Conference object . 2005
26 references, page 1 of 2

1. E. Albert, G. Puebla, and M. Hermenegildo. An Abstract Interpretation-based Approach to Mobile Code Safety. In Proc. of Compiler Optimization meets Compiler Verification (COCV'04), Electronic Notes in Theoretical Computer Science 132(1), pages 113-129. Elsevier - North Holland, April 2005.

2. E. Albert, G. Puebla, and M. Hermenegildo. Abstraction-Carrying Code. In llth International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR'04), number 3452 in LNAI, pages 380-397. Springer-Verlag, March 2005.

3. M. Bruynooghe. A Practical Framework for the Abstract Interpretation of Logic Programs. Journal of Logic Programming, 10:91-124, 1991. [OpenAIRE]

4. F. Bueno, D. Cabeza, M. Carro, M. Hermenegildo, P. López-García, and G. Puebla. The Ciao Prolog System. Reference Manual (vi.8). Technical Report CLIP4/2002.1, School of Computer Science, UPM, 2002. Available at h t t p : / / c l i p . d i a . f i . u p m . e s / S o f t w a r e / C i a o / .

5. F. Bueno, P. Deransart, W. Drabent, G. Ferrand, M. Hermenegildo, J. Maluszynski, and G. Puebla. On the Role of Semantic Approximations in Validation and Diagnosis of Constraint Logic Programs. In Proc. of the 3rd. Int'l Workshop on Automated Debugging-AADEBUG'97, pages 155-170, Linkoping, Sweden, May 1997. U. of Linkoping Press. [OpenAIRE]

6. B. Le Charlier and P. Van Hentenryck. Experimental Evaluation of a Generic Abstract Interpretation Algorithm for Prolog. ACM Transactions on Programming Languages and Systems, 16(1):35-101, 1994.

7. P. Cousot and R. Cousot. Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. of POPL'77, pages 238-252, 1977.

8. S. K. Debray. Static Inference of Modes and Data Dependencies in Logic Programs. ACM Transactions on Programming Languages and Systems, ll(3):418-450, 1989. [OpenAIRE]

9. S.K. Debray, P. López-García, M. Hermenegildo, and N.-W. Lin. Estimating the Computational Cost of Logic Programs. In Proc. of SAS'94, number 864 in LNCS, pages 255-265. Springer-Verlag, 1994. Invited Talk. [OpenAIRE]

10. S.K. Debray, P. López-García, M. Hermenegildo, and N.-W. Lin. Lower Bound Cost Estimation for Logic Programs. In Proc. of ILPS'97, pages 291-305. MIT Press, Cambridge, MA, 1997. [OpenAIRE]

11. J. Gallagher and D. de Waal. Fast and Precise Regular Approximations of Logic Programs. In Proc. of ICLP'94, pages 599-613. MIT Press, 1994.

12. J. Gallagher and G. Puebla. Abstract Interpretation over Non-Deterministic Finite Tree Autómata for Set-Based Analysis of Logic Programs. In Proc. of PADL'02, LNCS, pages 243-261, 2002.

13. M. Hermenegildo, G. Puebla, F. Bueno, and P. López-García. Program Development Using Abstract Interpretation (and The Ciao System Preprocessor). In Proc. of SAS'03, pages 127-152. Springer LNCS 2694, 2003.

14. M. Hermenegildo, G. Puebla, K. Marriott, and P. Stuckey. Incremental Analysis of Constraint Logic Programs. ACM Transactions on Programming Languages and Systems, 22(2):187-223, March 2000. [OpenAIRE]

15. K. Klohs and U. Kastens. Memory Requirements of Java Bytecode Verification on Limited Devices. In Proc. of Compüer Optimization meets Compiler Verification (COCV'04), 2004.

26 references, page 1 of 2
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue