Mostrar el registro sencillo del ítem
dc.contributor.author | Vidal Oriola, Germán Francisco | es_ES |
dc.date.accessioned | 2016-03-07T08:57:37Z | |
dc.date.available | 2016-03-07T08:57:37Z | |
dc.date.issued | 2015-05 | |
dc.identifier.issn | 0167-6423 | |
dc.identifier.uri | http://hdl.handle.net/10251/61507 | |
dc.description.abstract | Program termination is a relevant property that has been extensively studied in the context of many different formalisms and programming languages. Traditional approaches to proving termination are usually based on inspecting the source code. Recently, a new semantics-based approach has emerged, which typically follows a two-stage scheme: first, a finite data structure representing the computation space of the program is built; then, termination is analyzed by inspecting the transitions in this data structure using traditional, syntax-based techniques. Unfortunately, this approach is still specific to a programming language and semantics. In this work, we present instead a general, high-level framework that follows the semanticsbased approach to proving termination. In particular, we focus on the first stage and advocate the use of symbolic execution, together with appropriate subsumption and abstraction operators, for producing a finite representation of the computations of a program. Hopefully, this higher level approach will provide useful insights for designing new semantics-based termination tools for particular programming languages. © 2015 Elsevier B.V. All rights reserved. | es_ES |
dc.description.sponsorship | This work has been partially supported by the EU (FEDER) and the Spanish Ministerio de Economia y Competitividad (Secretaria de Estado de Investigacion, Desarrollo e Innovacion) under grant TIN2013-44742-C4-1-R and by the Generalitat Valenciana under grant PROMETEO/2011/052. | en_EN |
dc.language | Inglés | es_ES |
dc.publisher | Elsevier | es_ES |
dc.relation.ispartof | Science of Computer Programming | es_ES |
dc.rights | Reserva de todos los derechos | es_ES |
dc.subject | Program termination | es_ES |
dc.subject | Symbolic execution | es_ES |
dc.subject | Program analysis | es_ES |
dc.subject.classification | LENGUAJES Y SISTEMAS INFORMATICOS | es_ES |
dc.title | Symbolic execution as a basis for termination analysis | es_ES |
dc.type | Artículo | es_ES |
dc.identifier.doi | 10.1016/j.scico.2015.01.007 | |
dc.relation.projectID | info:eu-repo/grantAgreement/MINECO//TIN2013-44742-C4-1-R/ES/VALIDACION ASISTIDA DE PROGRAMAS MEDIANTE METODOS PRECISOS Y RIGUROSOS PARA UNA INGENIERIA DEL SOFTWARE ROBUSTA/ | 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 | Vidal Oriola, GF. (2015). Symbolic execution as a basis for termination analysis. Science of Computer Programming. 102:142-157. https://doi.org/10.1016/j.scico.2015.01.007 | es_ES |
dc.description.accrualMethod | S | es_ES |
dc.relation.publisherversion | http://dx.doi.org/10.1016/j.scico.2015.01.007 | es_ES |
dc.description.upvformatpinicio | 142 | es_ES |
dc.description.upvformatpfin | 157 | es_ES |
dc.type.version | info:eu-repo/semantics/publishedVersion | es_ES |
dc.description.volume | 102 | es_ES |
dc.relation.senia | 301931 | es_ES |
dc.contributor.funder | Ministerio de Economía y Competitividad | es_ES |
dc.contributor.funder | Generalitat Valenciana | es_ES |