Abstract Diagnosis for tccp using a Linear Temporal Logic

Resumen:

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.

Palabras Clave:

Autor(es):

• M. Comini {}
  Dipartimento di Matematica e Informatica, U. di Udine
  
• L. Titolo {}
  Dipartimento di Matematica e Informatica, U. di Udine
  
• A. Villanueva {}
  DSIC, Universitat Politécnica de Valéncia
  

Handle:

Descargas:

Este artículo tiene una licencia de uso CreativeCommons - Reconocimiento (by)

Descarga el artículo haciendo click aquí.

Ver la referencia en formato Bibtex