Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/14209
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Barros, José Bernardo | - |
dc.contributor.author | Cruz, Daniela da | - |
dc.contributor.author | Henriques, Pedro Rangel | - |
dc.contributor.author | Pinto, Jorge Sousa | - |
dc.date.accessioned | 2011-11-09T14:51:22Z | - |
dc.date.available | 2011-11-09T14:51:22Z | - |
dc.date.issued | 2012 | - |
dc.identifier.issn | 0934-5043 | por |
dc.identifier.uri | https://hdl.handle.net/1822/14209 | - |
dc.description.abstract | This paper revisits the idea of slicing programs based on their axiomatic semantics, rather than using criteria based on control/data dependencies. We show how the forward propagation of preconditions and the backward propagation of postconditions can be combined in a new slicing algorithm that is more precise than the existing specification-based algorithms. The algorithm is based on (i) a precise test for removable statements, and (ii) the construction of a \emph{slice graph}, a program control flow graph extended with semantic labels and additional edges that ``short-circuit'' removable commands. It improves on previous approaches in two aspects: it does not fail to identify removable commands; and it produces the smallest possible slice that can be obtained (in a sense that will be made precise). Iteration is handled through the use of loop invariants and variants to ensure termination. The paper also discusses in detail applications of these forms of slicing, including the elimination of (conditionally) unreachable and dead code, and compares them to other related notions. | por |
dc.description.sponsorship | Fundação para a Ciência e a Tecnologia (FCT) | por |
dc.language.iso | eng | por |
dc.publisher | Springer | por |
dc.relation | info:eu-repo/grantAgreement/FCT/5876-PPCDTI/108995/PT | - |
dc.rights | openAccess | por |
dc.subject | Program slicing | por |
dc.subject | Program analysis | por |
dc.subject | Verification conditions | por |
dc.subject | Control flow graphs | por |
dc.title | Assertion-based slicing and slice graphs | por |
dc.type | article | - |
dc.peerreviewed | yes | por |
dc.relation.publisherversion | The original publication is available at http://www.springerlink.com/content/j45m7rtv2563r135/ | por |
sdum.publicationstatus | in publication | por |
oaire.citationStartPage | 217 | por |
oaire.citationEndPage | 248 | por |
oaire.citationIssue | 2 | por |
oaire.citationTitle | Formal Aspects of Computing | por |
oaire.citationVolume | 24 | por |
dc.identifier.doi | 10.1007/s00165-011-0196-1 | - |
dc.subject.wos | Science & Technology | por |
sdum.journal | Formal Aspects of Computing | por |
Aparece nas coleções: | HASLab - Artigos em revistas internacionais DI/CCTC - Artigos (papers) |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
SEFM2010specSlicing-journal.pdf | Documento principal | 422,49 kB | Adobe PDF | Ver/Abrir |