Mostrar el registro sencillo del ítem
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 |