- -

A program analysis framework for tccp based on abstract interpretation

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

A program analysis framework for tccp based on abstract interpretation

Mostrar el registro sencillo del ítem

Ficheros en el ítem

dc.contributor.author Comini, Marco es_ES
dc.contributor.author Gallardo, Maria-del-Mar es_ES
dc.contributor.author Titolo, Laura es_ES
dc.contributor.author Villanueva, Alicia es_ES
dc.date.accessioned 2020-10-21T03:31:24Z
dc.date.available 2020-10-21T03:31:24Z
dc.date.issued 2017-05 es_ES
dc.identifier.issn 0934-5043 es_ES
dc.identifier.uri http://hdl.handle.net/10251/152716
dc.description.abstract [EN] The timed concurrent constraint language (tccp) is a timed extension of the concurrent constraint paradigm. tccp was defined to model reactive systems, where infinite behaviors arise naturally. In previous works, a semantic framework and abstract diagnosis method for the language have been defined. On the basis of that semantic framework, this paper proposes an abstract semantics that, together with a widening operator, is suitable for the definition of different analyses for tccp programs. The abstract semantics is correct and can be represented as a finite graph where each node represents a hypothetical (abstract) computational step of the program. The widening operator allows us to guarantee the convergence of the abstract fixpoint computation. es_ES
dc.description.sponsorship This author has been supported by the Andalusian Excellence Project P11-TIC-7659. This work has been partially supported by the EU (FEDER) and the Spanish MINECO under grants TIN 2015-69175-C4-1-R and TIN 2013-45732-C4-1-P and by Generalitat Valenciana PROMETEOII/2015/013 es_ES
dc.language Inglés es_ES
dc.publisher Springer-Verlag es_ES
dc.relation.ispartof Formal Aspects of Computing es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Concurrent constraint paradigm es_ES
dc.subject Abstract interpretation es_ES
dc.subject Abstract semantics es_ES
dc.subject Widening operators es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title A program analysis framework for tccp based on abstract interpretation es_ES
dc.type Artículo es_ES
dc.identifier.doi 10.1007/s00165-016-0409-8 es_ES
dc.relation.projectID info:eu-repo/grantAgreement/Junta de Andalucía//P11-TIC-7659/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/MINECO//TIN2013-45732-C4-1-P/ES/UNA APROXIMACION DECLARATIVA AL MODELADO, ANALISIS Y RESOLUCION DE PROBLEMAS/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GVA//PROMETEOII%2F2015%2F013/ES/SmartLogic: Logic Technologies for Software Security and Performance/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/MINECO//TIN2015-69175-C4-1-R/ES/SOLUCIONES EFECTIVAS BASADAS EN LA LOGICA/ es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation Comini, M.; Gallardo, M.; Titolo, L.; Villanueva, A. (2017). A program analysis framework for tccp based on abstract interpretation. Formal Aspects of Computing. 29(3):531-557. https://doi.org/10.1007/s00165-016-0409-8 es_ES
dc.description.accrualMethod S es_ES
dc.relation.publisherversion https://doi.org/10.1007/s00165-016-0409-8 es_ES
dc.description.upvformatpinicio 531 es_ES
dc.description.upvformatpfin 557 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.description.volume 29 es_ES
dc.description.issue 3 es_ES
dc.relation.pasarela S\326711 es_ES
dc.contributor.funder Junta de Andalucía es_ES
dc.contributor.funder Generalitat Valenciana es_ES
dc.contributor.funder Ministerio de Economía, Industria y Competitividad es_ES
dc.description.references Alpuente M, Gallardo MM, Pimentel E, Villanueva A (2006) A semantic framework for the abstract model checking of tccp programs. Theor Comput Scie 346(1): 58–95 es_ES
dc.description.references Bagnara R, Hill PM., Ricci E, Zaffanella E (2005) Precise widening operators for convex polyhedra. Sci Comput Program 58(1–2):28–56 es_ES
dc.description.references Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on principles of programming languages, Los Angeles, California, January 17–19. ACM Press, New York, pp 238–252 es_ES
dc.description.references Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: CAV, Lecture Notes in Computer Science, vol 1855. Springer, pp 154–169 es_ES
dc.description.references Comini M, Gallardo MM, Titolo L, Villanueva A (2015) Abstract Analysis of Universal Properties for tccp. In: Falaschi M (ed) Logic-based Program Synthesis and Transformation, 25th International Symposium, LOPSTR 2015. Revised Selected Papers, Lecture Notes in Computer Science, vol 9527. Springer, pp 163–178 es_ES
dc.description.references Comini M, Titolo L, Villanueva A (2011) Abstract diagnosis for timed concurrent constraint programs. Theory Pract Logic Programm 11(4-5):487–502 es_ES
dc.description.references Comini M, Titolo L, Villanueva A (2013) A condensed goal-independent bottom-up fixpoint modeling the behavior of tccp. Technical report, DSIC, Universitat Politècnica de València. http://riunet.upv.es/handle/10251/34328 es_ES
dc.description.references de Boer FS, Gabbrielli M, Meo MC (2000) A timed concurrent constraint language. Inf Comput 161(1): 45–83 es_ES
dc.description.references Falaschi M, Gabbrielli M, Marriott K, Palamidessi C (1993) Compositional analysis for concurrent constraint programming. In: Proceedings of the eighth annual IEEE symposium on logic in computer science, Los Alamitos, CA, USA, IEEE Computer Society Press, pp 210–221 es_ES
dc.description.references Falaschi M, Olarte C, Palamidessi C (2015) Abstract interpretation of temporal concurrent constraint programs. Theory and Pract Logic Program (TPLP) 15(3): 312–357 es_ES
dc.description.references Falaschi M, Villanueva A (2006) Automatic verification of timed concurrent constraint programs. Theory Pract Logic Program 6(3): 265–300 es_ES
dc.description.references Gallardo MM, Merino P, Pimentel E (2002) Refinement of LTL formulas for abstract model checking. In: Static analysis, 9th international symposium, SAS 2002, Madrid, Spain, September 17–20, 2002, Proceedings, pp 395–410 es_ES
dc.description.references Saraswat VA (1993) Concurrent constraint programming. The MIT Press, Cambridge es_ES
dc.description.references Saraswat VA, Rinard M, Panangaden P (1991) The semantic foundations of concurrent constraint programming. In: Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, New York, pp 333–352 es_ES
dc.description.references Zaffanella E, Giacobazzi R, Levi G (1997) Abstracting synchronization in concurrent constraint programming. J Funct Logic Program (6) es_ES


Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem