Abstract Analysis of Universal Properties for tccp

  • Marco Comini
  • María del Mar Gallardo
  • Laura TitoloEmail author
  • Alicia Villanueva
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9527)


The Timed Concurrent Constraint Language (tccp) is a time extension of the concurrent constraint paradigm of Saraswat. 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 has 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 computational step of the program containing approximated information for the variables. The widening operator allows us to guarantee the convergence of the abstract fixpoint computation.


Concurrent constraint paradigm Abstract analysis 


  1. 1.
    Alpuente, M., Gallardo, M.M., Pimentel, E., Villanueva, A.: A semantic framework for the abstract model checking of tccp programs. Theor. Comput. Sci. 346(1), 58–95 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Sci Comput. Program. 58(1–2), 28–56 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Comini, M., Titolo, L., Villanueva, A.: Abstract diagnosis for timed concurrent constraint programs. Theor. Pract. Log. Program. 11(4–5), 487–502 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Comini, M., Titolo, L., Villanueva, A.: A condensed goal-independent bottom-up fixpoint modeling the behavior of tccp. Technical report, DSIC, Universitat Politècnica de València (2013).
  5. 5.
    Cousot, P., Cousot, R.: 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, pp. 238–252. ACM Press, New York (1977)Google Scholar
  6. 6.
    de Boer, F.S., Gabbrielli, M., Meo, M.C.: A timed concurrent constraint language. Inf. Comput. 161(1), 45–83 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Falaschi, M. Gabbrielli, M., Marriott, K., Palamidessi, C.: Compositional analysis for concurrent constraint programming. In: Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science, pp. 210–221. IEEE Computer Society Press, Los Alamitos (1993)Google Scholar
  8. 8.
    Falaschi, M., Olarte, C., Palamidessi, C.: Abstract interpretation of temporal concurrent constraint programs. Theor. Pract. Log. Program. (TPLP) 15(3), 312–357 (2015)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Falaschi, M., Villanueva, A.: Automatic verification of timed concurrent constraint programs. Theor. Pract. Log. Program. 6(3), 265–300 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Saraswat, V.A.: Concurrent Constraint Programming. The MIT Press, Cambridge (1993)zbMATHGoogle Scholar
  11. 11.
    Zaffanella, E., Giacobazzi, R., Levi, G.: Abstracting synchronization in concurrent constraint programming. J. Funct. Log. Program. 6, 1997 (1997)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Marco Comini
    • 1
  • María del Mar Gallardo
    • 2
  • Laura Titolo
    • 2
    Email author
  • Alicia Villanueva
    • 3
  1. 1.DIMIUniversità Degli Studi di UdineUdineItaly
  2. 2.LCCUniversidad de MálagaMálagaSpain
  3. 3.DSICUniversitat Politècnica de ValènciaValenciaSpain

Personalised recommendations