- -

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 2015-03-10T11:17:20Z
dc.date.available 2015-03-10T11:17:20Z
dc.date.issued 2014-07
dc.identifier.issn 1471-0684
dc.identifier.uri http://hdl.handle.net/10251/47912
dc.description.abstract [EN] 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 represents 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 sometimes 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 interpretation 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.description.sponsorship This work has been partially supported by the eu (feder) and the Spanish mec/micinn, ref. tin 2010-21062-c02-0, and by Generalitat Valenciana, ref. prometeo2011/052.
dc.language Inglés es_ES
dc.publisher Cambridge University Press es_ES
dc.relation MEC/MICINN/TIN2010-21062-C02-0 es_ES
dc.relation GV/PROMETEO2011/052 es_ES
dc.relation.ispartof Theory and Practice of Logic Programming es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Concurrent constraint paradigm es_ES
dc.subject Linear temporal logic es_ES
dc.subject Abstract diagnosis es_ES
dc.subject Decision procedures es_ES
dc.subject Program verification es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Abstract Diagnosis for tccp using a Linear Temporal Logic es_ES
dc.type Artículo es_ES
dc.type Comunicación en congreso
dc.identifier.doi 10.1017/S1471068414000349
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. Theory and Practice of Logic Programming. 14(4-5):787-801. doi:10.1017/S1471068414000349 es_ES
dc.description.accrualMethod Senia es_ES
dc.relation.conferencename 30th International Conference on Logic Programming
dc.relation.conferencedate July, 2014
dc.relation.conferenceplace Viena, Austria
dc.relation.publisherversion http://dx.doi.org/10.1017/S1471068414000349 es_ES
dc.description.upvformatpinicio 787 es_ES
dc.description.upvformatpfin 801 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.description.volume 14 es_ES
dc.description.issue 4-5 es_ES
dc.relation.senia 280266
dc.contributor.funder Ministerio de Ciencia e Innovación
dc.contributor.funder Generalitat Valenciana


This item appears in the following Collection(s)

Show simple item record