View in EDS

Conditional termination of loops over heap-allocated data.

Saved in:
Bibliographic Details
Title: Conditional termination of loops over heap-allocated data.
Authors: Albert, Elvira1 elvira@sip.ucm.es, Arenas, Puri1 puri@sip.ucm.es, Genaim, Samir1 samir@fdi.ucm.es, Puebla, Germán2 german@fi.upm.es, Román-Díez, Guillermo2 groman@fi.upm.es
Source: Science of Computer Programming. Oct2014, Vol. 92 Issue Part A, p2-24. 23p.
Subjects: Computer software termination, Data analysis, Computational complexity, Information retrieval, Java programming language, Mathematical proofs
Abstract: Abstract: Static analysis which takes into account the values of data stored in the heap is considered complex and computationally intractable in practice. Thus, most static analyzers do not keep track of object fields nor of array contents, i.e., they are heap-insensitive. In this article, we propose locality conditions for soundly tracking heap-allocated data in Java (bytecode) programs, by means of ghost non-heap allocated variables. This way, heap-insensitive analysis over the transformed program can infer information on the original heap-allocated data without sacrificing efficiency. If the locality conditions cannot be proven unconditionally, we seek to generate aliasing preconditions which, when they hold in the initial state, guarantee the termination of the program. Experimental results show that we greatly improve the accuracy w.r.t. a heap-insensitive analysis while the overhead introduced is reasonable. [Copyright &y& Elsevier]
Copyright of Science of Computer Programming is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 96345548
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Conditional termination of loops over heap-allocated data.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Albert%2C+Elvira%22">Albert, Elvira</searchLink><relatesTo>1</relatesTo><i> elvira@sip.ucm.es</i><br /><searchLink fieldCode="AR" term="%22Arenas%2C+Puri%22">Arenas, Puri</searchLink><relatesTo>1</relatesTo><i> puri@sip.ucm.es</i><br /><searchLink fieldCode="AR" term="%22Genaim%2C+Samir%22">Genaim, Samir</searchLink><relatesTo>1</relatesTo><i> samir@fdi.ucm.es</i><br /><searchLink fieldCode="AR" term="%22Puebla%2C+Germán%22">Puebla, Germán</searchLink><relatesTo>2</relatesTo><i> german@fi.upm.es</i><br /><searchLink fieldCode="AR" term="%22Román-Díez%2C+Guillermo%22">Román-Díez, Guillermo</searchLink><relatesTo>2</relatesTo><i> groman@fi.upm.es</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Science+of+Computer+Programming%22">Science of Computer Programming</searchLink>. Oct2014, Vol. 92 Issue Part A, p2-24. 23p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Computer+software+termination%22">Computer software termination</searchLink><br /><searchLink fieldCode="DE" term="%22Data+analysis%22">Data analysis</searchLink><br /><searchLink fieldCode="DE" term="%22Computational+complexity%22">Computational complexity</searchLink><br /><searchLink fieldCode="DE" term="%22Information+retrieval%22">Information retrieval</searchLink><br /><searchLink fieldCode="DE" term="%22Java+programming+language%22">Java programming language</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+proofs%22">Mathematical proofs</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Abstract: Static analysis which takes into account the values of data stored in the heap is considered complex and computationally intractable in practice. Thus, most static analyzers do not keep track of object fields nor of array contents, i.e., they are heap-insensitive. In this article, we propose locality conditions for soundly tracking heap-allocated data in Java (bytecode) programs, by means of ghost non-heap allocated variables. This way, heap-insensitive analysis over the transformed program can infer information on the original heap-allocated data without sacrificing efficiency. If the locality conditions cannot be proven unconditionally, we seek to generate aliasing preconditions which, when they hold in the initial state, guarantee the termination of the program. Experimental results show that we greatly improve the accuracy w.r.t. a heap-insensitive analysis while the overhead introduced is reasonable. [Copyright &y& Elsevier]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Science of Computer Programming is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=96345548
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1016/j.scico.2013.04.006
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 23
        StartPage: 2
    Subjects:
      – SubjectFull: Computer software termination
        Type: general
      – SubjectFull: Data analysis
        Type: general
      – SubjectFull: Computational complexity
        Type: general
      – SubjectFull: Information retrieval
        Type: general
      – SubjectFull: Java programming language
        Type: general
      – SubjectFull: Mathematical proofs
        Type: general
    Titles:
      – TitleFull: Conditional termination of loops over heap-allocated data.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Albert, Elvira
      – PersonEntity:
          Name:
            NameFull: Arenas, Puri
      – PersonEntity:
          Name:
            NameFull: Genaim, Samir
      – PersonEntity:
          Name:
            NameFull: Puebla, Germán
      – PersonEntity:
          Name:
            NameFull: Román-Díez, Guillermo
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 15
              M: 10
              Text: Oct2014
              Type: published
              Y: 2014
          Identifiers:
            – Type: issn-print
              Value: 01676423
          Numbering:
            – Type: volume
              Value: 92
            – Type: issue
              Value: Part A
          Titles:
            – TitleFull: Science of Computer Programming
              Type: main
ResultId 1