Búsqueda avanzada

El autor L. Titolo ha publicado 2 artículo(s):

1 - Abstract Diagnosis for tccp using a Linear Temporal Logic

This extended abstract is a summary of [5], where we provided an automatic decision method to check whether a given property, specified in a linear temporal logic, is valid w.r.t. a tccp program. Our proposal (based on abstract interpretation techniques) does not require to build any model of the program, in constrast with standard verification methods such as model checking. Our results guarantee correctness but, as usual when using an abstract semantics, completeness is lost.

Autores: M. Comini / L. Titolo / A. Villanueva / 
Palabras Clave:

2 - Abstract Diagnosis for Timed Concurrent Constraint programs Abstract

This short paper is a summary of the published paper [CTV11] where a general framework for the debugging of tccp programs is defined. To this end, a new compact, bottom-up semantics for the language that is well suited for debugging and verification purposes in the context of reactive systems was presented. In order to effectively implement the technique, we also provided an abstract semantics.

Autores: M. Comini / L. Titolo / A. Villanueva / 
Palabras Clave: abstract diagnosis - abstract interpretation - concurrent constraint paradigm - denotational semantics