Mostrar el registro sencillo del í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 |