- -

Symbolic execution as a basis for termination analysis

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

Symbolic execution as a basis for termination analysis

Show simple item record

Files in this item

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 EU (FEDER) es_ES
dc.relation Spanish Ministerio de Economia y Competitividad (Secretaria de Estado de Investigacion, Desarrollo e Innovacion) [TIN2013-44742-C4-1-R] es_ES
dc.relation Generalitat Valenciana [PROMETEO/2011/052] 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.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. doi: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


This item appears in the following Collection(s)

Show simple item record