Mostrar el registro sencillo del ítem
dc.contributor.author | Alpuente Frasnedo, María | es_ES |
dc.contributor.author | Escobar Román, Santiago | es_ES |
dc.contributor.author | Ballis, Demis | es_ES |
dc.contributor.author | Sapiña-Sanchis, Julia | es_ES |
dc.date.accessioned | 2023-07-21T18:04:00Z | |
dc.date.available | 2023-07-21T18:04:00Z | |
dc.date.issued | 2022-05 | es_ES |
dc.identifier.issn | 1471-0684 | es_ES |
dc.identifier.uri | http://hdl.handle.net/10251/195317 | |
dc.description.abstract | [EN] This paper introduces Presto, a symbolic partial evaluator for Maude's rewriting logic theories that can improve system analysis and verification. In Presto, the automated optimization of a conditional rewrite theory R (whose rules define the concurrent transitions of a system) is achieved by partially evaluating, with respect to the rules of R, an underlying, companion equational logic theory E that specifies the algebraic structure of the system states of R. This can be particularly useful for specializing an overly general equational theory E whose operators may obey complex combinations of associativity, commutativity, and/or identity axioms, when being plugged into a host rewrite theory R as happens, for instance, in protocol analysis, where sophisticated equational theories for cryptography are used. Presto implements different unfolding operators that are based on folding variant narrowing (the symbolic engine of Maude's equational theories). When combined with an appropriate abstraction algorithm, they allow the specialization to be adapted to the theory termination behavior and bring significant improvement while ensuring strong correctness and termination of the specialization. We demonstrate the effectiveness of Presto in several examples of protocol analysis where it achieves a significant speed-up. Actually, the transformation provided by Presto may cut down an infinite folding variant narrowing space to a finite one, and moreover, some of the costly algebraic axioms and rule conditions may be eliminated as well. As far as we know, this is the first partial evaluator for Maude that respects the semantics of functional, logic, concurrent, and object-oriented computations. | es_ES |
dc.description.sponsorship | This research was partially supported by TAILOR, a project funded by EU Horizon 2020 research and innovation programme under GA No 952215, grant RTI2018-094403-B-C32 funded by MCIN/AEI/10.13039/501100011033 and by "ERDF A way of making Europe", and by Generalitat Valenciana under grant PROMETEO/2019/098. Julia Sapiña has been supported by the Generalitat Valenciana APOSTD/2019/127 grant. | es_ES |
dc.language | Inglés | es_ES |
dc.publisher | Cambridge University Press | es_ES |
dc.relation.ispartof | Theory and Practice of Logic Programming | es_ES |
dc.rights | Reconocimiento (by) | es_ES |
dc.subject | Multi-paradigm declarative programming | es_ES |
dc.subject | Partial evaluation | es_ES |
dc.subject | Rewriting logic | es_ES |
dc.subject | Narrowing | es_ES |
dc.subject.classification | LENGUAJES Y SISTEMAS INFORMATICOS | es_ES |
dc.title | Symbolic Specialization of Rewriting Logic Theories with Presto | es_ES |
dc.type | Artículo | es_ES |
dc.identifier.doi | 10.1017/S1471068421000600 | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/RTI2018-094403-B-C32/ES/RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES/ | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/GENERALITAT VALENCIANA//PROMETEO%2F2019%2F098//DEEPTRUST/ | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/EC/H2020/952215/EU | es_ES |
dc.relation.projectID | info:eu-repo/grantAgreement/GVA//APOSTD%2F2019%2F127//CONTRATO POSDOCTORAL GVA-SAPIÑA SANCHIS. PROYECTO: METODOS SIMBOLICOS AVANZADOS PARA EL ANALISIS DE SEGURIDAD DE PROTOCOLOS/ | es_ES |
dc.rights.accessRights | Abierto | es_ES |
dc.contributor.affiliation | Universitat Politècnica de València. Escola Tècnica Superior d'Enginyeria Informàtica | es_ES |
dc.description.bibliographicCitation | Alpuente Frasnedo, M.; Escobar Román, S.; Ballis, D.; Sapiña-Sanchis, J. (2022). Symbolic Specialization of Rewriting Logic Theories with Presto. Theory and Practice of Logic Programming. 22(3):444-495. https://doi.org/10.1017/S1471068421000600 | es_ES |
dc.description.accrualMethod | S | es_ES |
dc.relation.publisherversion | https://doi.org/10.1017/S1471068421000600 | es_ES |
dc.description.upvformatpinicio | 444 | es_ES |
dc.description.upvformatpfin | 495 | es_ES |
dc.type.version | info:eu-repo/semantics/publishedVersion | es_ES |
dc.description.volume | 22 | es_ES |
dc.description.issue | 3 | es_ES |
dc.relation.pasarela | S\453327 | es_ES |
dc.contributor.funder | GENERALITAT VALENCIANA | es_ES |
dc.contributor.funder | AGENCIA ESTATAL DE INVESTIGACION | es_ES |
dc.contributor.funder | European Regional Development Fund | es_ES |
dc.contributor.funder | COMISION DE LAS COMUNIDADES EUROPEA | es_ES |