- -

Abstract Diagnosis for tccp using a Linear Temporal Logic

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

Abstract Diagnosis for tccp using a Linear Temporal Logic

Show simple item record

Files in this item

dc.contributor.author Comini, Marco es_ES
dc.contributor.author Titolo, Laura es_ES
dc.contributor.author Villanueva García, Alicia es_ES
dc.date.accessioned 2014-02-15T01:09:12Z
dc.date.available 2014-02-15T01:09:12Z
dc.date.issued 2014-02-15
dc.identifier.uri http://hdl.handle.net/10251/35695
dc.description.abstract Automatic techniques for program verification usually suffer the well-known state explosion problem. Most of the classical approaches are based on browsing the structure of some form of model (which rep- resents the behavior of the program) to check if a given specification is valid. This implies that a part of the model has to be built, and some- times the needed fragment is quite huge. In this work, we provide an alternative 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 interpreta- tion techniques) does not require to build any model at all. Our results guarantee correctness but, as usual when using an abstract semantics, completeness is lost. es_ES
dc.format.extent 35 es_ES
dc.language Inglés es_ES
dc.publisher Universitat Politècnica de València es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Concurrent constraint paradigm es_ES
dc.subject Linear temporal logic
dc.subject Abstract diagnosis
dc.subject Decision procedures
dc.subject Program verification
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Abstract Diagnosis for tccp using a Linear Temporal Logic es_ES
dc.type Informe es_ES
dc.relation.projectID info:eu-repo/grantAgreement/MICINN//TIN2010-21062-C02-02/ES/SWEETLOGICS-UPV/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GVA//PROMETEO%2F2011%2F052/ES/LOGICEXTREME: TECNOLOGIA LOGICA Y SOFTWARE SEGURO/ es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation Comini, M.; Titolo, L.; Villanueva García, A. (2014). Abstract Diagnosis for tccp using a Linear Temporal Logic. Universitat Politècnica de València. http://hdl.handle.net/10251/35695 es_ES
dc.contributor.funder Ministerio de Ciencia e Innovación es_ES
dc.contributor.funder Generalitat Valenciana es_ES


This item appears in the following Collection(s)

Show simple item record