Abstract interpretation of temporal concurrent constraint programs

Falaschi, Moreno; Palamidessi, Catuscia; Vega, Carlos Alberto Olarte

Abstract interpretation of temporal concurrent constraint programs

Página do item simplificado Estatísticas

dc.contributor.author	Falaschi, Moreno
dc.contributor.author	Palamidessi, Catuscia
dc.contributor.author	Vega, Carlos Alberto Olarte
dc.date.accessioned	2020-08-03T20:04:37Z
dc.date.available	2020-08-03T20:04:37Z
dc.date.issued	2014
dc.description.resumo	Timed Concurrent Constraint Programming (tcc) is a declarative model for concurrency offering a logic for specifying reactive systems, i.e., systems that continuously interact with the environment. The universal tcc formalism (utcc) is an extension of tcc with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. In this paper we consider the denotational semantics for tcc, and extend it to a “collecting” semantics for utcc based on closure operators over sequences of constraints. Relying on this semantics, we formalize a general framework for data flow analyses of tcc and utcc programs by abstract interpretation techniques. The concrete and abstract semantics that we propose are compositional, thus allowing us to reduce the complexity of data flow analyses. We show that our method is sound and parametric with respect to the abstract domain. Thus, different analyses can be performed by instantiating the framework. We illustrate how it is possible to reuse abstract domains previously defined for logic programming to perform, for instance, a groundness analysis for tcc programs. We show the applicability of this analysis in the context of reactive systems. Furthermore, we also make use of the abstract semantics to exhibit a secrecy flaw in a security protocol. We also show how it is possible to make an analysis which may show that tcc programs are suspension-free. This can be useful for several purposes, such as for optimizing compilation or for debugging	pt_BR
dc.identifier.citation	FALASCHI, Moreno; OLARTE, Carlos; PALAMIDESSI, Catuscia. Abstract interpretation of temporal concurrent constraint programs. Theory and Practice of Logic Programming, [S.L.], v. 15, n. 3, p. 312-357, 10 fev. 2014. Disponível em: https://www.cambridge.org/core/journals/theory-and-practice-of-logic-programming/article/abstract-interpretation-of-temporal-concurrent-constraint-programs/79AB54B8007AA797C1631A461FD7CE2B. Acesso em: 30 jul. 2020. https://doi.org/10.1017/S1471068413000641	pt_BR
dc.identifier.doi	10.1017/S1471068413000641
dc.identifier.issn	1475-3081
dc.identifier.uri	https://repositorio.ufrn.br/jspui/handle/123456789/29777
dc.language	en	pt_BR
dc.publisher	Cambridge University Press	pt_BR
dc.subject	Timed concurrent constraint programming	pt_BR
dc.subject	Process calculi	pt_BR
dc.subject	Abstract interpretation	pt_BR
dc.subject	Denotational semantics	pt_BR
dc.subject	Reactive systems	pt_BR
dc.title	Abstract interpretation of temporal concurrent constraint programs	pt_BR
dc.type	article	pt_BR