Descending chains and narrowing on template abstract domains View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

2018-09

AUTHORS

Gianluca Amato, Simone Di Nardo Di Maio, Maria Chiara Meo, Francesca Scozzari

ABSTRACT

A static analysis by abstract interpretation is typically composed of an ascending phase followed by a descending one. The descending phase is used to improve the precision of the analysis after that a post-fixpoint has been reached. Termination is often guaranteed by using narrowing operators, especially on numerical domains which are generally endowed with infinite descending chains. Under the hypothesis of dealing with reducible flow graphs, we provide an abstract semantics which improves the analysis precision and we show that, for a large class of numerical abstract domains over integer variables (such as intervals, octagons, template parallelotopes and template polyhedra), infinite descending chains cannot arise and we can safely omit narrowing. The abstract semantics is a slight variation of the standard one and can be easily implemented. We also provide an acceleration procedure which ensures termination of the descending phase without narrowing even with non-reducible graphs. Finally, we propose a new family of weak narrowing operators for real variables which improve the analysis precision. More... »

PAGES

521-545

References to SciGraph publications

Journal

TITLE

Acta Informatica

ISSUE

6

VOLUME

55

Author Affiliations

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/s00236-016-0291-0

DOI

http://dx.doi.org/10.1007/s00236-016-0291-0

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1024535957


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

JSON-LD is the canonical representation for SciGraph data.

TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

[
  {
    "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
    "about": [
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0101", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Pure Mathematics", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/01", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Mathematical Sciences", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "University of Chieti-Pescara", 
          "id": "https://www.grid.ac/institutes/grid.412451.7", 
          "name": [
            "Universit\u00e0 di Chieti-Pescara, Pescara, Italy"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Amato", 
        "givenName": "Gianluca", 
        "id": "sg:person.016462567676.84", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016462567676.84"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "University of Chieti-Pescara", 
          "id": "https://www.grid.ac/institutes/grid.412451.7", 
          "name": [
            "Universit\u00e0 di Chieti-Pescara, Pescara, Italy"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Di Nardo Di Maio", 
        "givenName": "Simone", 
        "id": "sg:person.012461627166.53", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012461627166.53"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "University of Chieti-Pescara", 
          "id": "https://www.grid.ac/institutes/grid.412451.7", 
          "name": [
            "Universit\u00e0 di Chieti-Pescara, Pescara, Italy"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Meo", 
        "givenName": "Maria Chiara", 
        "id": "sg:person.010516504205.98", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010516504205.98"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "University of Chieti-Pescara", 
          "id": "https://www.grid.ac/institutes/grid.412451.7", 
          "name": [
            "Universit\u00e0 di Chieti-Pescara, Pescara, Italy"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Scozzari", 
        "givenName": "Francesca", 
        "id": "sg:person.012164226533.26", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012164226533.26"
        ], 
        "type": "Person"
      }
    ], 
    "citation": [
      {
        "id": "sg:pub.10.1007/978-3-642-33125-1_15", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1003090017", 
          "https://doi.org/10.1007/978-3-642-33125-1_15"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/512760.512770", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1005273787"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/11823230_10", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1006274110", 
          "https://doi.org/10.1007/11823230_10"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/11823230_10", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1006274110", 
          "https://doi.org/10.1007/11823230_10"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/b105073", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1010132446", 
          "https://doi.org/10.1007/b105073"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/b105073", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1010132446", 
          "https://doi.org/10.1007/b105073"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/567752.567778", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1018302391"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/978-3-642-38856-9_4", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1025359431", 
          "https://doi.org/10.1007/978-3-642-38856-9_4"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/bfb0039704", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1025687928", 
          "https://doi.org/10.1007/bfb0039704"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/j.jsc.2011.12.052", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1026289310"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/11513988_46", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1031221055", 
          "https://doi.org/10.1007/11513988_46"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/11513988_46", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1031221055", 
          "https://doi.org/10.1007/11513988_46"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/978-3-319-19249-9_5", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1035868563", 
          "https://doi.org/10.1007/978-3-319-19249-9_5"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/j.entcs.2012.09.003", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1037069304"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/512950.512973", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1045819695"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/j.scico.2015.12.005", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1046468742"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/1961204.1961207", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1046770579"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/s10990-006-8609-1", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1049136525", 
          "https://doi.org/10.1007/s10990-006-8609-1"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/3-540-45013-0_7", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1049269195", 
          "https://doi.org/10.1007/3-540-45013-0_7"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.2168/lmcs-8(3:29)2012", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1069151221"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/2491956.2462190", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1098844320"
        ], 
        "type": "CreativeWork"
      }
    ], 
    "datePublished": "2018-09", 
    "datePublishedReg": "2018-09-01", 
    "description": "A static analysis by abstract interpretation is typically composed of an ascending phase followed by a descending one. The descending phase is used to improve the precision of the analysis after that a post-fixpoint has been reached. Termination is often guaranteed by using narrowing operators, especially on numerical domains which are generally endowed with infinite descending chains. Under the hypothesis of dealing with reducible flow graphs, we provide an abstract semantics which improves the analysis precision and we show that, for a large class of numerical abstract domains over integer variables (such as intervals, octagons, template parallelotopes and template polyhedra), infinite descending chains cannot arise and we can safely omit narrowing. The abstract semantics is a slight variation of the standard one and can be easily implemented. We also provide an acceleration procedure which ensures termination of the descending phase without narrowing even with non-reducible graphs. Finally, we propose a new family of weak narrowing operators for real variables which improve the analysis precision.", 
    "genre": "research_article", 
    "id": "sg:pub.10.1007/s00236-016-0291-0", 
    "inLanguage": [
      "en"
    ], 
    "isAccessibleForFree": false, 
    "isPartOf": [
      {
        "id": "sg:journal.1133515", 
        "issn": [
          "0001-5903", 
          "1432-0525"
        ], 
        "name": "Acta Informatica", 
        "type": "Periodical"
      }, 
      {
        "issueNumber": "6", 
        "type": "PublicationIssue"
      }, 
      {
        "type": "PublicationVolume", 
        "volumeNumber": "55"
      }
    ], 
    "name": "Descending chains and narrowing on template abstract domains", 
    "pagination": "521-545", 
    "productId": [
      {
        "name": "readcube_id", 
        "type": "PropertyValue", 
        "value": [
          "74e3d32ac21f38c560e6d3dacc35a106f94fd3f4da83da7c355b2e05f761d3eb"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/s00236-016-0291-0"
        ]
      }, 
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1024535957"
        ]
      }
    ], 
    "sameAs": [
      "https://doi.org/10.1007/s00236-016-0291-0", 
      "https://app.dimensions.ai/details/publication/pub.1024535957"
    ], 
    "sdDataset": "articles", 
    "sdDatePublished": "2019-04-11T09:53", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-uberresearch-data-dimensions-target-20181106-alternative/cleanup/v134/2549eaecd7973599484d7c17b260dba0a4ecb94b/merge/v9/a6c9fde33151104705d4d7ff012ea9563521a3ce/jats-lookup/v90/0000000347_0000000347/records_89793_00000001.jsonl", 
    "type": "ScholarlyArticle", 
    "url": "https://link.springer.com/10.1007%2Fs00236-016-0291-0"
  }
]
 

Download the RDF metadata as:  json-ld nt turtle xml License info

HOW TO GET THIS DATA PROGRAMMATICALLY:

JSON-LD is a popular format for linked data which is fully compatible with JSON.

curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/s00236-016-0291-0'

N-Triples is a line-based linked data format ideal for batch operations.

curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/s00236-016-0291-0'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s00236-016-0291-0'

RDF/XML is a standard XML format for linked data.

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/s00236-016-0291-0'


 

This table displays all metadata directly associated to this object as RDF triples.

145 TRIPLES      21 PREDICATES      45 URIs      19 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/s00236-016-0291-0 schema:about anzsrc-for:01
2 anzsrc-for:0101
3 schema:author N87ad75f0c0c8494a8df1532b5cecbc80
4 schema:citation sg:pub.10.1007/11513988_46
5 sg:pub.10.1007/11823230_10
6 sg:pub.10.1007/3-540-45013-0_7
7 sg:pub.10.1007/978-3-319-19249-9_5
8 sg:pub.10.1007/978-3-642-33125-1_15
9 sg:pub.10.1007/978-3-642-38856-9_4
10 sg:pub.10.1007/b105073
11 sg:pub.10.1007/bfb0039704
12 sg:pub.10.1007/s10990-006-8609-1
13 https://doi.org/10.1016/j.entcs.2012.09.003
14 https://doi.org/10.1016/j.jsc.2011.12.052
15 https://doi.org/10.1016/j.scico.2015.12.005
16 https://doi.org/10.1145/1961204.1961207
17 https://doi.org/10.1145/2491956.2462190
18 https://doi.org/10.1145/512760.512770
19 https://doi.org/10.1145/512950.512973
20 https://doi.org/10.1145/567752.567778
21 https://doi.org/10.2168/lmcs-8(3:29)2012
22 schema:datePublished 2018-09
23 schema:datePublishedReg 2018-09-01
24 schema:description A static analysis by abstract interpretation is typically composed of an ascending phase followed by a descending one. The descending phase is used to improve the precision of the analysis after that a post-fixpoint has been reached. Termination is often guaranteed by using narrowing operators, especially on numerical domains which are generally endowed with infinite descending chains. Under the hypothesis of dealing with reducible flow graphs, we provide an abstract semantics which improves the analysis precision and we show that, for a large class of numerical abstract domains over integer variables (such as intervals, octagons, template parallelotopes and template polyhedra), infinite descending chains cannot arise and we can safely omit narrowing. The abstract semantics is a slight variation of the standard one and can be easily implemented. We also provide an acceleration procedure which ensures termination of the descending phase without narrowing even with non-reducible graphs. Finally, we propose a new family of weak narrowing operators for real variables which improve the analysis precision.
25 schema:genre research_article
26 schema:inLanguage en
27 schema:isAccessibleForFree false
28 schema:isPartOf N854391a3689c4fe2aa501c5d50b272ca
29 Nde636252e69b4108ac08bb12233bfb4c
30 sg:journal.1133515
31 schema:name Descending chains and narrowing on template abstract domains
32 schema:pagination 521-545
33 schema:productId N205daade9a34443398157aa81a394636
34 N9c80d5658272413287d40f3b3bb58bdc
35 Na765aea4d0b149f786ac40da827d97d2
36 schema:sameAs https://app.dimensions.ai/details/publication/pub.1024535957
37 https://doi.org/10.1007/s00236-016-0291-0
38 schema:sdDatePublished 2019-04-11T09:53
39 schema:sdLicense https://scigraph.springernature.com/explorer/license/
40 schema:sdPublisher Nbfe5e69ca6fb426e8a593e932cda9f95
41 schema:url https://link.springer.com/10.1007%2Fs00236-016-0291-0
42 sgo:license sg:explorer/license/
43 sgo:sdDataset articles
44 rdf:type schema:ScholarlyArticle
45 N205daade9a34443398157aa81a394636 schema:name doi
46 schema:value 10.1007/s00236-016-0291-0
47 rdf:type schema:PropertyValue
48 N43e29ec76020491887e3a39dd5a43b67 rdf:first sg:person.010516504205.98
49 rdf:rest Na0dabc7c586a42c3b808548cdbbb5d51
50 N854391a3689c4fe2aa501c5d50b272ca schema:issueNumber 6
51 rdf:type schema:PublicationIssue
52 N87ad75f0c0c8494a8df1532b5cecbc80 rdf:first sg:person.016462567676.84
53 rdf:rest Na7d32aeeb4d240778116600bf4678f82
54 N9c80d5658272413287d40f3b3bb58bdc schema:name dimensions_id
55 schema:value pub.1024535957
56 rdf:type schema:PropertyValue
57 Na0dabc7c586a42c3b808548cdbbb5d51 rdf:first sg:person.012164226533.26
58 rdf:rest rdf:nil
59 Na765aea4d0b149f786ac40da827d97d2 schema:name readcube_id
60 schema:value 74e3d32ac21f38c560e6d3dacc35a106f94fd3f4da83da7c355b2e05f761d3eb
61 rdf:type schema:PropertyValue
62 Na7d32aeeb4d240778116600bf4678f82 rdf:first sg:person.012461627166.53
63 rdf:rest N43e29ec76020491887e3a39dd5a43b67
64 Nbfe5e69ca6fb426e8a593e932cda9f95 schema:name Springer Nature - SN SciGraph project
65 rdf:type schema:Organization
66 Nde636252e69b4108ac08bb12233bfb4c schema:volumeNumber 55
67 rdf:type schema:PublicationVolume
68 anzsrc-for:01 schema:inDefinedTermSet anzsrc-for:
69 schema:name Mathematical Sciences
70 rdf:type schema:DefinedTerm
71 anzsrc-for:0101 schema:inDefinedTermSet anzsrc-for:
72 schema:name Pure Mathematics
73 rdf:type schema:DefinedTerm
74 sg:journal.1133515 schema:issn 0001-5903
75 1432-0525
76 schema:name Acta Informatica
77 rdf:type schema:Periodical
78 sg:person.010516504205.98 schema:affiliation https://www.grid.ac/institutes/grid.412451.7
79 schema:familyName Meo
80 schema:givenName Maria Chiara
81 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010516504205.98
82 rdf:type schema:Person
83 sg:person.012164226533.26 schema:affiliation https://www.grid.ac/institutes/grid.412451.7
84 schema:familyName Scozzari
85 schema:givenName Francesca
86 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012164226533.26
87 rdf:type schema:Person
88 sg:person.012461627166.53 schema:affiliation https://www.grid.ac/institutes/grid.412451.7
89 schema:familyName Di Nardo Di Maio
90 schema:givenName Simone
91 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012461627166.53
92 rdf:type schema:Person
93 sg:person.016462567676.84 schema:affiliation https://www.grid.ac/institutes/grid.412451.7
94 schema:familyName Amato
95 schema:givenName Gianluca
96 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016462567676.84
97 rdf:type schema:Person
98 sg:pub.10.1007/11513988_46 schema:sameAs https://app.dimensions.ai/details/publication/pub.1031221055
99 https://doi.org/10.1007/11513988_46
100 rdf:type schema:CreativeWork
101 sg:pub.10.1007/11823230_10 schema:sameAs https://app.dimensions.ai/details/publication/pub.1006274110
102 https://doi.org/10.1007/11823230_10
103 rdf:type schema:CreativeWork
104 sg:pub.10.1007/3-540-45013-0_7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1049269195
105 https://doi.org/10.1007/3-540-45013-0_7
106 rdf:type schema:CreativeWork
107 sg:pub.10.1007/978-3-319-19249-9_5 schema:sameAs https://app.dimensions.ai/details/publication/pub.1035868563
108 https://doi.org/10.1007/978-3-319-19249-9_5
109 rdf:type schema:CreativeWork
110 sg:pub.10.1007/978-3-642-33125-1_15 schema:sameAs https://app.dimensions.ai/details/publication/pub.1003090017
111 https://doi.org/10.1007/978-3-642-33125-1_15
112 rdf:type schema:CreativeWork
113 sg:pub.10.1007/978-3-642-38856-9_4 schema:sameAs https://app.dimensions.ai/details/publication/pub.1025359431
114 https://doi.org/10.1007/978-3-642-38856-9_4
115 rdf:type schema:CreativeWork
116 sg:pub.10.1007/b105073 schema:sameAs https://app.dimensions.ai/details/publication/pub.1010132446
117 https://doi.org/10.1007/b105073
118 rdf:type schema:CreativeWork
119 sg:pub.10.1007/bfb0039704 schema:sameAs https://app.dimensions.ai/details/publication/pub.1025687928
120 https://doi.org/10.1007/bfb0039704
121 rdf:type schema:CreativeWork
122 sg:pub.10.1007/s10990-006-8609-1 schema:sameAs https://app.dimensions.ai/details/publication/pub.1049136525
123 https://doi.org/10.1007/s10990-006-8609-1
124 rdf:type schema:CreativeWork
125 https://doi.org/10.1016/j.entcs.2012.09.003 schema:sameAs https://app.dimensions.ai/details/publication/pub.1037069304
126 rdf:type schema:CreativeWork
127 https://doi.org/10.1016/j.jsc.2011.12.052 schema:sameAs https://app.dimensions.ai/details/publication/pub.1026289310
128 rdf:type schema:CreativeWork
129 https://doi.org/10.1016/j.scico.2015.12.005 schema:sameAs https://app.dimensions.ai/details/publication/pub.1046468742
130 rdf:type schema:CreativeWork
131 https://doi.org/10.1145/1961204.1961207 schema:sameAs https://app.dimensions.ai/details/publication/pub.1046770579
132 rdf:type schema:CreativeWork
133 https://doi.org/10.1145/2491956.2462190 schema:sameAs https://app.dimensions.ai/details/publication/pub.1098844320
134 rdf:type schema:CreativeWork
135 https://doi.org/10.1145/512760.512770 schema:sameAs https://app.dimensions.ai/details/publication/pub.1005273787
136 rdf:type schema:CreativeWork
137 https://doi.org/10.1145/512950.512973 schema:sameAs https://app.dimensions.ai/details/publication/pub.1045819695
138 rdf:type schema:CreativeWork
139 https://doi.org/10.1145/567752.567778 schema:sameAs https://app.dimensions.ai/details/publication/pub.1018302391
140 rdf:type schema:CreativeWork
141 https://doi.org/10.2168/lmcs-8(3:29)2012 schema:sameAs https://app.dimensions.ai/details/publication/pub.1069151221
142 rdf:type schema:CreativeWork
143 https://www.grid.ac/institutes/grid.412451.7 schema:alternateName University of Chieti-Pescara
144 schema:name Università di Chieti-Pescara, Pescara, Italy
145 rdf:type schema:Organization
 




Preview window. Press ESC to close (or click here)


...