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. https://doi.org/10.1017/S1471068414000349
Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/10251/47912
Title:
|
Abstract Diagnosis for tccp using a Linear Temporal Logic
|
Author:
|
Comini, Marco
Titolo, Laura
Villanueva García, Alicia
|
UPV Unit:
|
Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació
|
Issued date:
|
|
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 ...[+]
[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.
[-]
|
Subjects:
|
Concurrent constraint paradigm
,
Linear temporal logic
,
Abstract diagnosis
,
Decision procedures
,
Program verification
|
Copyrigths:
|
Reserva de todos los derechos
|
Source:
|
Theory and Practice of Logic Programming. (issn:
1471-0684
)
|
DOI:
|
10.1017/S1471068414000349
|
Publisher:
|
Cambridge University Press
|
Publisher version:
|
http://dx.doi.org/10.1017/S1471068414000349
|
Conference name:
|
30th International Conference on Logic Programming
|
Conference place:
|
Viena, Austria
|
Conference date:
|
July, 2014
|
Project ID:
|
info:eu-repo/grantAgreement/MICINN//TIN2010-21062-C02-02/ES/SWEETLOGICS-UPV/
info:eu-repo/grantAgreement/GVA//PROMETEO%2F2011%2F052/ES/LOGICEXTREME: TECNOLOGIA LOGICA Y SOFTWARE SEGURO/
|
Thanks:
|
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.
|
Type:
|
Artículo
Comunicación en congreso
|