{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T04:04:50Z","timestamp":1749960290935,"version":"3.41.0"},"reference-count":16,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2017,5,1]],"date-time":"2017-05-01T00:00:00Z","timestamp":1493596800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100006461","name":"Agencia de Innovaci\u00f3n y Desarrollo de Andaluc\u00eda","doi-asserted-by":"publisher","award":["P11-TIC-7659"],"award-info":[{"award-number":["P11-TIC-7659"]}],"id":[{"id":"10.13039\/501100006461","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100007136","name":"Secretar\u00eda de Estado de Investigaci\u00f3n, Desarrollo e Innovaci\u00f3n","doi-asserted-by":"publisher","award":["TIN 2015-69175-C4-1-R","TIN 2013-45732-C4-1-P"],"award-info":[{"award-number":["TIN 2015-69175-C4-1-R","TIN 2013-45732-C4-1-P"]}],"id":[{"id":"10.13039\/501100007136","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Generalitat Valenciana (ES)","award":["PROMETEOII\/2015\/013"],"award-info":[{"award-number":["PROMETEOII\/2015\/013"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The timed concurrent constraint language (<jats:italic>tccp<\/jats:italic>) is a timed extension of the concurrent constraint paradigm.<jats:italic>tccp<\/jats:italic>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<jats:italic>tccp<\/jats:italic>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.<\/jats:p>","DOI":"10.1007\/s00165-016-0409-8","type":"journal-article","created":{"date-parts":[[2017,1,17]],"date-time":"2017-01-17T06:30:58Z","timestamp":1484634658000},"page":"531-557","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A program analysis framework for<i>tccp<\/i>based on abstract interpretation"],"prefix":"10.1145","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8069-3411","authenticated-orcid":false,"given":"Marco","family":"Comini","sequence":"first","affiliation":[{"name":"Dipartimento di Scienze Matematiche, Informatiche e Fisiche, Universit\u00e0 degli Studi di Udine, Udine, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mar\u00eda-del-Mar","family":"Gallardo","sequence":"additional","affiliation":[{"name":"LCC, Universidad de M\u00e1laga, M\u00e1laga, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laura","family":"Titolo","sequence":"additional","affiliation":[{"name":"National Institute of Aerospace, Hampton, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1090-5009","authenticated-orcid":false,"given":"Alicia","family":"Villanueva","sequence":"additional","affiliation":[{"name":"DSIC, Universitat Polit\u00e8cnica de Val\u00e8ncia, Valencia, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.08.009"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Bagnara R Hill PM. Ricci E Zaffanella E (2005) Precise widening operators for convex polyhedra. Sci Comput Program 58(1\u20132):28\u201356","DOI":"10.1016\/j.scico.2005.02.003"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"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\u201319. ACM Press New York pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"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\u2013169","DOI":"10.1007\/10722167_15"},{"key":"#cr-split#-e_1_2_1_2_5_2.1","doi-asserted-by":"crossref","unstructured":"Comini M Gallardo MM Titolo L Villanueva A (2015) Abstract Analysis of Universal Properties for tccp. In: Falaschi M","DOI":"10.1007\/978-3-319-27436-2_10"},{"key":"#cr-split#-e_1_2_1_2_5_2.2","unstructured":"(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"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Comini M Titolo L Villanueva A (2011) Abstract diagnosis for timed concurrent constraint programs. Theory Pract Logic Programm 11(4-5):487\u2013502","DOI":"10.1017\/S1471068411000135"},{"key":"e_1_2_1_2_7_2","unstructured":"Comini M Titolo L Villanueva A (2013) A condensed goal-independent bottom-up fixpoint modeling the behavior of tccp. Technical report DSIC Universitat Polit\u00e8cnica de Val\u00e8ncia. http:\/\/riunet.upv.es\/handle\/10251\/34328"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2879"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"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\u2013221","DOI":"10.1109\/LICS.1993.287586"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068413000641"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068406002675"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"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\u201320 2002 Proceedings pp 395\u2013410","DOI":"10.1007\/3-540-45789-5_28"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/151204"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"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\u2013352","DOI":"10.1145\/99583.99627"},{"key":"e_1_2_1_2_15_2","unstructured":"Zaffanella E Giacobazzi R Levi G (1997) Abstracting synchronization in concurrent constraint programming. J Funct Logic Program (6)"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0409-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0409-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0409-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0409-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T14:53:37Z","timestamp":1749912817000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0409-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5]]},"references-count":16,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,5]]}},"alternative-id":["10.1007\/s00165-016-0409-8"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0409-8","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2017,5]]}}}