@article {AGPV08,
	title = {An Abstract Analysis Framework for Synchronous Concurrent Languages based on source-to-source Transformation},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {206},
	year = {2008},
	pages = {3{\textendash}21},
	abstract = {A pretty wide range of concurrent programming languages have been developed over the years. Coming from different programming traditions, concurrent languages differ in many respects, though all share the common aspect to expose parallelism to programmers. In order to provide language level support to programming with more than one process, a few basic concurrency primitives are often combined to provide the main language constructs, sometimes making different
assumptions. In this paper, we analyze the most common primitives and related semantics for the class of synchronous concurrent programming languages, i.e., languages with a global mechanism of processes synchronization. Then, we present a generic framework for approximating the semantics of the main constructs which applies to both, declarative as well as imperative concurrent programming languages. We determine the conditions which ensure the correctness of the approximation, so that the resulting abstract semantics safely supports program analysis and verification. Finally, we ascertain the conditions that make it possible to implement the abstraction by a source to source transformation of the language semantics.},
	author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. and Alicia Villanueva}
}
@proceedings {AGPV07,
	title = {An Abstract Analysis Framework for Synchronous Concurrent Languages based on source-to-source Transformation},
	journal = {Actas de las VII Jornadas de Programaci{\'o}n y Lenguajes (PROLE{\textquoteright}07)},
	year = {2007},
	month = {sep},
	pages = {81{\textendash}92},
	abstract = {A pretty wide range of concurrent programming languages have been developed over the years. Coming from different programming traditions, concurrent languages differ in many respects, though all share the common aspect to expose parallelism to programmers. In order to provide language level support to programming with more than one process, a few basic concurrency primitives are often combined to provide the main language constructs, sometimes making different
assumptions. In this paper, we analyze the most common primitives and related semantics for the class of synchronous concurrent programming languages, i.e., languages with a global mechanism of processes synchronization. Then, we present a generic framework for approximating the semantics of the main constructs which applies to both, declarative as well as imperative concurrent programming languages. We determine the conditions which ensure the correctness of the approximation, so that the resulting abstract semantics safely supports program analysis and verification. Finally, we ascertain the conditions that make it possible to implement the abstraction by a source to source transformation of the language semantics.},
	author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. and Alicia Villanueva}
}
@article {AGV07,
	title = {A Framework for Timed Concurrent Constraint Programming with External Functions},
	journal = {Electronic Notes in Theoretical Computer Science},
	volume = {188C},
	year = {2007},
	pages = {143{\textendash}155},
	abstract = {The Timed Concurrent Constraint programming language (tccp in short),  was introduced for modeling reactive systems. This language allows one to model in a very intuitive way typical ingredients of  these systems such as timeouts, preemptions, etc. However, there is no natural way for modeling other desirable features such as functional computations, for example for calculating arithmetic results. In fact, although it is certainly possible to implement such kind of operations,  each single step of the computation takes time in tccp, and avoiding interferences with the intended overall behavior of the (reactive) system is quite involved.

In this paper, we propose an extension of tccp for modeling instantaneous computations which  improves the  expressiveness of the language, in the sense that operations that are cumbersome to implement in pure tccp, are executed by calling an efficient, external functional engine, while the tccp programmer can focus on the pure, and usually more complex, reactive part of the system. We also describe a case study which motivates the work, and discuss how the new capability presented here can also be used as a new tool for developers from the verification point of view.},
	keywords = {functions, tccp},
	author = {Maria Alpuente and Gramlich, B. and Alicia Villanueva}
}
@article {AGPV06,
	title = {A Real-Time Logic for tccp verification},
	journal = {Journal of Universal Computer Science},
	volume = {12},
	number = {11},
	year = {2006},
	month = {November},
	pages = {1551{\textendash}1573},
	keywords = {cc, Logic},
	author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. and Alicia Villanueva}
}
@article {AGV06-tr,
	title = {Timed Concurrent Constraint programming with External Functions},
	number = {DSIC-II/13/06},
	year = {2006},
	publisher = {DSIC, UPV},
	author = {Maria Alpuente and Gramlich, B. and Alicia Villanueva}
}
@proceedings {AGV06,
	title = {Timed Concurrent Constraint Programming with Instantaneous Computations},
	journal = {Actas de las VI Jornadas de Programaci},
	year = {2006},
	address = {Sitges, Barcelona, Spain},
	author = {Maria Alpuente and Gramlich, B. and Alicia Villanueva}
}
@article {AGPV05,
	title = {A Semantic Framework for the Abstract Model Checking of tccp programs},
	journal = {{Theoretical Computer Science}},
	volume = {346},
	year = {2005},
	pages = {58{\textendash}95},
	keywords = {Abstraction, cc, model checking},
	author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. and Alicia Villanueva}
}
@proceedings {AGPV05c,
	title = {Verifying Real-Time Properties of tccp Programs},
	journal = {Proc. of the Quintas Jornadas sobre Programaci{\'o}n y Lenguajes, PROLE{\textquoteright}05, 2005},
	year = {2005},
	pages = {85{\textendash}94},
	author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. and Alicia Villanueva},
	editor = {L{\'o}pez-Fraguas, F.J.}
}
@article {AGPV04,
	title = {Abstract Model Checking of tccp programs},
	journal = {Electronic Notes in Theoretical Computer Science (ENTCS)},
	volume = {112},
	year = {2004},
	pages = {19{\textendash}36},
	keywords = {Abstraction, cc, model checking},
	author = {Maria Alpuente and Gallardo, M.M. and Pimentel, E. and Alicia Villanueva}
}
@article {CominiGLV99,
	title = {Abstract Interpretation based Verification of Logic Programs},
	journal = {Science of Computer Programming},
	volume = {49},
	number = {1{\textendash}3},
	year = {2003},
	pages = {89{\textendash}123},
	abstract = {This paper is an overview of our results on the application of abstract interpretation concepts to various problems related to the verification of logic programs. These include the systematic design of semantics modeling various proof methods and the characterization of assertions as abstract domains.},
	keywords = {Abstract Diagnosis, Abstract Interpretation, Abstract Verification, Assertion Language, Inductive Verification, Logic Programming},
	author = {Marco Comini and Roberta Gori and Giorgio Levi and Volpe, P.}
}
@proceedings {CominiGL00b,
	title = {Assertion based Inductive Verification Methods for Logic Programs},
	journal = {Proceedings of MFCSIT{\textquoteright}2000},
	volume = {40},
	year = {2001},
	note = {Available at URL: {\href{http://www.elsevier.nl/locate/entcs/volume40.html} {\texttt{http://www.elsevier.nl/locate/entcs/volume40.html}}}},
	pages = {1{\textendash}18},
	publisher = {Elsevier Science Publishers},
	abstract = {This paper is an overview of our results on the application of abstract interpretation concepts to the derivation of a verification method for logic programs. These include the systematic design of semantics modeling various proof methods and the characterization of assertions as abstract domains. We first apply the verification framework defined in [CominiGLV99] to derive inductive sufficient conditions for partial correctness. Then the domain of assertions is formalized as an abstract domain. We can therefore derive an assertion based verification method. We finally show two methods based on different assertion languages: a decidable assertion language and Horn clause logic used as assertion language.},
	keywords = {Abstract Interpretation, Assertion Language, Inductive Verification, Transformation of logic programs},
	author = {Marco Comini and Roberta Gori and Giorgio Levi},
	editor = {A. K. Seda}
}
@proceedings {CominiGL01,
	title = {How to Transform an Analyzer into a Verifier},
	journal = {Logic for Programming and Automated Reasoning. Proceedings of the 8th International Conference (LPAR{\textquoteright}01)},
	volume = {2250},
	year = {2001},
	pages = {595{\textendash}609},
	publisher = {Springer-Verlag},
	address = {Berlin},
	abstract = {In this paper we push forward the idea of applying the abstract interpretation concepts to the problem of verification of programs. We consider the theory of abstract verification as proposed in [CominiGLV99entcs,CominiGLV99] and we show how it is possible to transform static analyzers with some suitable properties to obtain automatic verification tools based on sufficient verification conditions. We prove that the approach is general and flexible by showing three different verification tools based on different domains of types for functional, logic programming and CLP programming. The verifier for functional programs is obtained from a static analyzer which implements one of the polymorphic type domains introduced by Cousot [Cousot97c]. The one for logic programs is obtained from a static analyzer on a type domain designed by Codish and Lagoon [CodishL98], while the verifier for CLP programs is obtained starting from the type analyzer described in [DrabentP98].},
	keywords = {Abstract Interpretation, Abstract Verification, Inductive Verification},
	author = {Marco Comini and Roberta Gori and Giorgio Levi},
	editor = {Nieuwenhuis, R. and Voronkov, A.}
}
@proceedings {CominiGL00a,
	title = {Logic programs as specifications in the inductive verification of logic programs},
	journal = {Declarative Programming {\textendash} Selected Papers from AGP 2000},
	volume = {48},
	year = {2001},
	note = {Available at URL: {\href{http://www.elsevier.nl/locate/entcs/volume48.html} {\texttt{http://www.elsevier.nl/locate/entcs/volume48.html}}}},
	pages = {1{\textendash}16},
	publisher = {Elsevier Science Publishers},
	abstract = {n this paper we define a new verification method based on an assertion language able to express properties defined by the user through a logic program. We first apply the verification framework defined in [CominiGLV99] to derive sufficient inductive conditions to prove partial correctness. Then we show how the resulting conditions can be proved using program transformation techniques.},
	keywords = {Abstract Interpretation, Inductive Verification, Transformation of logic programs},
	author = {Marco Comini and Roberta Gori and Giorgio Levi},
	editor = {Agostino Dovier and Maria Chiara Meo and Omicini, A.}
}
@proceedings {FPV01,
	title = {Time Limited Model Checking},
	journal = {Proceedings of International Workshop on Specification Analysis and Validation for Emerging Technologies in Computational Logic (SAVE{\textquoteright}01)},
	year = {2001},
	keywords = {cc, model checking},
	author = {Moreno Falaschi and Policriti, A. and Alicia Villanueva},
	editor = {Delzanno, G. and Etalle, S. and Gabbrielli, M.}
}
