Abstraction-Based Partial Deduction for Solving Inverse Problems — A Transformational Approach to Software Verification View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2000-01-28

AUTHORS

Robert Glück , Michael Leuschel

ABSTRACT

We present an approach to software verification by program inversion, exploiting recent progress in the field of automatic program transformation, partial deduction and abstract interpretation. Abstraction-based partial deduction can work on infinite state spaces and produce finite representations of infinite solution sets. We illustrate the potential of this approach for infinite model checking of safety properties. More... »

PAGES

93-100

References to SciGraph publications

  • 2005-06-26. The essence of program transformation by partial evaluation and driving in LOGIC, LANGUAGE AND COMPUTATION
  • 1998. Detecting unsolvable queries for definite logic programs in PRINCIPLES OF DECLARATIVE PROGRAMMING
  • 1998. Staging static analyses using abstraction-based program specialization in PRINCIPLES OF DECLARATIVE PROGRAMMING
  • 1997. Efficient model checking using tabled resolution in COMPUTER AIDED VERIFICATION
  • 1997-05. Running programs backwards: The logical inversion of imperative computation in FORMAL ASPECTS OF COMPUTING
  • 1996. Logic program specialisation: How to be more specific in PROGRAMMING LANGUAGES: IMPLEMENTATIONS, LOGICS, AND PROGRAMS
  • Book

    TITLE

    Perspectives of System Informatics

    ISBN

    978-3-540-67102-2
    978-3-540-46562-1

    Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/3-540-46562-6_8

    DOI

    http://dx.doi.org/10.1007/3-540-46562-6_8

    DIMENSIONS

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


    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/0802", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Computation Theory and Mathematics", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Information and Computing Sciences", 
            "type": "DefinedTerm"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "University of Copenhagen", 
              "id": "https://www.grid.ac/institutes/grid.5254.6", 
              "name": [
                "DIKU, Department of Computer Science, University of Copenhagen, DK-2100, Copenhagen, Denmark"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Gl\u00fcck", 
            "givenName": "Robert", 
            "id": "sg:person.010754010217.31", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010754010217.31"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "University of Southampton", 
              "id": "https://www.grid.ac/institutes/grid.5491.9", 
              "name": [
                "Department of Electronics and Computer Science, University of Southampton, SO17 1BJ, Southampton, UK"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Leuschel", 
            "givenName": "Michael", 
            "id": "sg:person.011762452312.13", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011762452312.13"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/3-540-61756-6_82", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1001809528", 
              "https://doi.org/10.1007/3-540-61756-6_82"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf01211087", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1008568428", 
              "https://doi.org/10.1007/bf01211087"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bf01211087", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1008568428", 
              "https://doi.org/10.1007/bf01211087"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/242223.242257", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1014368099"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1017/s0956796800000757", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1016061186"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/136035.136043", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1018110957"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0056612", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1018243572", 
              "https://doi.org/10.1007/bfb0056612"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/191839.191927", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1018675534"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/169683.174155", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1022267651"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0032402", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1027875008", 
              "https://doi.org/10.1007/bfb0032402"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0032402", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1027875008", 
              "https://doi.org/10.1007/bfb0032402"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/bfb0056611", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1029972945", 
              "https://doi.org/10.1007/bfb0056611"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-63166-6_16", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1037672054", 
              "https://doi.org/10.1007/3-540-63166-6_16"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/271510.271525", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1037743749"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1017/s0956796800001167", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1038404271"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/5397.5399", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1053218197"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2000-01-28", 
        "datePublishedReg": "2000-01-28", 
        "description": "We present an approach to software verification by program inversion, exploiting recent progress in the field of automatic program transformation, partial deduction and abstract interpretation. Abstraction-based partial deduction can work on infinite state spaces and produce finite representations of infinite solution sets. We illustrate the potential of this approach for infinite model checking of safety properties.", 
        "editor": [
          {
            "familyName": "Bj\u00f8ner", 
            "givenName": "Dines", 
            "type": "Person"
          }, 
          {
            "familyName": "Broy", 
            "givenName": "Manfred", 
            "type": "Person"
          }, 
          {
            "familyName": "Zamulin", 
            "givenName": "Alexandre V.", 
            "type": "Person"
          }
        ], 
        "genre": "chapter", 
        "id": "sg:pub.10.1007/3-540-46562-6_8", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": false, 
        "isPartOf": {
          "isbn": [
            "978-3-540-67102-2", 
            "978-3-540-46562-1"
          ], 
          "name": "Perspectives of System Informatics", 
          "type": "Book"
        }, 
        "name": "Abstraction-Based Partial Deduction for Solving Inverse Problems \u2014 A Transformational Approach to Software Verification", 
        "pagination": "93-100", 
        "productId": [
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/3-540-46562-6_8"
            ]
          }, 
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "26559af15fccb3c5a5218f7feb475ba1cef9942cb25d6f98ed580592c6c0cb18"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1008046482"
            ]
          }
        ], 
        "publisher": {
          "location": "Berlin, Heidelberg", 
          "name": "Springer Berlin Heidelberg", 
          "type": "Organisation"
        }, 
        "sameAs": [
          "https://doi.org/10.1007/3-540-46562-6_8", 
          "https://app.dimensions.ai/details/publication/pub.1008046482"
        ], 
        "sdDataset": "chapters", 
        "sdDatePublished": "2019-04-16T05:50", 
        "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_89826_00000000.jsonl", 
        "type": "Chapter", 
        "url": "https://link.springer.com/10.1007%2F3-540-46562-6_8"
      }
    ]
     

    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/3-540-46562-6_8'

    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/3-540-46562-6_8'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/3-540-46562-6_8'

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

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/3-540-46562-6_8'


     

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

    133 TRIPLES      23 PREDICATES      40 URIs      19 LITERALS      8 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/3-540-46562-6_8 schema:about anzsrc-for:08
    2 anzsrc-for:0802
    3 schema:author Nc5767c3beb1941b7a819a23be9c163e7
    4 schema:citation sg:pub.10.1007/3-540-61756-6_82
    5 sg:pub.10.1007/3-540-63166-6_16
    6 sg:pub.10.1007/bf01211087
    7 sg:pub.10.1007/bfb0032402
    8 sg:pub.10.1007/bfb0056611
    9 sg:pub.10.1007/bfb0056612
    10 https://doi.org/10.1017/s0956796800000757
    11 https://doi.org/10.1017/s0956796800001167
    12 https://doi.org/10.1145/136035.136043
    13 https://doi.org/10.1145/169683.174155
    14 https://doi.org/10.1145/191839.191927
    15 https://doi.org/10.1145/242223.242257
    16 https://doi.org/10.1145/271510.271525
    17 https://doi.org/10.1145/5397.5399
    18 schema:datePublished 2000-01-28
    19 schema:datePublishedReg 2000-01-28
    20 schema:description We present an approach to software verification by program inversion, exploiting recent progress in the field of automatic program transformation, partial deduction and abstract interpretation. Abstraction-based partial deduction can work on infinite state spaces and produce finite representations of infinite solution sets. We illustrate the potential of this approach for infinite model checking of safety properties.
    21 schema:editor N74cc0ee30bf1466d8ac6fc66ced589b8
    22 schema:genre chapter
    23 schema:inLanguage en
    24 schema:isAccessibleForFree false
    25 schema:isPartOf Nab9f5d94d6574e94a16486e56a2a6d30
    26 schema:name Abstraction-Based Partial Deduction for Solving Inverse Problems — A Transformational Approach to Software Verification
    27 schema:pagination 93-100
    28 schema:productId N946c96edbdb8473c934dd0ee590d9bc1
    29 Ne90e4e69d624459dab96f36f6813b297
    30 Nf60377e30da74b8693304416d150c79f
    31 schema:publisher N836b4b997e2547b7b3fa70ccc6953416
    32 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008046482
    33 https://doi.org/10.1007/3-540-46562-6_8
    34 schema:sdDatePublished 2019-04-16T05:50
    35 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    36 schema:sdPublisher Nab5b75a246c8430eb614f97fc32582e5
    37 schema:url https://link.springer.com/10.1007%2F3-540-46562-6_8
    38 sgo:license sg:explorer/license/
    39 sgo:sdDataset chapters
    40 rdf:type schema:Chapter
    41 N3361febf59314543bae30f0dfab50c6c schema:familyName Zamulin
    42 schema:givenName Alexandre V.
    43 rdf:type schema:Person
    44 N4efa6a056e634687aeae5582e4ce2bae rdf:first N8ba0725b4e374c6ba6d9f433cb1b1e59
    45 rdf:rest N981629442c2149afaf1bf1ee1399a081
    46 N5d40d1b8d9124dd09687b3cb5584291c rdf:first sg:person.011762452312.13
    47 rdf:rest rdf:nil
    48 N6f7fa51529914c1a87ada11412f0a363 schema:familyName Bjøner
    49 schema:givenName Dines
    50 rdf:type schema:Person
    51 N74cc0ee30bf1466d8ac6fc66ced589b8 rdf:first N6f7fa51529914c1a87ada11412f0a363
    52 rdf:rest N4efa6a056e634687aeae5582e4ce2bae
    53 N836b4b997e2547b7b3fa70ccc6953416 schema:location Berlin, Heidelberg
    54 schema:name Springer Berlin Heidelberg
    55 rdf:type schema:Organisation
    56 N8ba0725b4e374c6ba6d9f433cb1b1e59 schema:familyName Broy
    57 schema:givenName Manfred
    58 rdf:type schema:Person
    59 N946c96edbdb8473c934dd0ee590d9bc1 schema:name readcube_id
    60 schema:value 26559af15fccb3c5a5218f7feb475ba1cef9942cb25d6f98ed580592c6c0cb18
    61 rdf:type schema:PropertyValue
    62 N981629442c2149afaf1bf1ee1399a081 rdf:first N3361febf59314543bae30f0dfab50c6c
    63 rdf:rest rdf:nil
    64 Nab5b75a246c8430eb614f97fc32582e5 schema:name Springer Nature - SN SciGraph project
    65 rdf:type schema:Organization
    66 Nab9f5d94d6574e94a16486e56a2a6d30 schema:isbn 978-3-540-46562-1
    67 978-3-540-67102-2
    68 schema:name Perspectives of System Informatics
    69 rdf:type schema:Book
    70 Nc5767c3beb1941b7a819a23be9c163e7 rdf:first sg:person.010754010217.31
    71 rdf:rest N5d40d1b8d9124dd09687b3cb5584291c
    72 Ne90e4e69d624459dab96f36f6813b297 schema:name doi
    73 schema:value 10.1007/3-540-46562-6_8
    74 rdf:type schema:PropertyValue
    75 Nf60377e30da74b8693304416d150c79f schema:name dimensions_id
    76 schema:value pub.1008046482
    77 rdf:type schema:PropertyValue
    78 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    79 schema:name Information and Computing Sciences
    80 rdf:type schema:DefinedTerm
    81 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
    82 schema:name Computation Theory and Mathematics
    83 rdf:type schema:DefinedTerm
    84 sg:person.010754010217.31 schema:affiliation https://www.grid.ac/institutes/grid.5254.6
    85 schema:familyName Glück
    86 schema:givenName Robert
    87 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010754010217.31
    88 rdf:type schema:Person
    89 sg:person.011762452312.13 schema:affiliation https://www.grid.ac/institutes/grid.5491.9
    90 schema:familyName Leuschel
    91 schema:givenName Michael
    92 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011762452312.13
    93 rdf:type schema:Person
    94 sg:pub.10.1007/3-540-61756-6_82 schema:sameAs https://app.dimensions.ai/details/publication/pub.1001809528
    95 https://doi.org/10.1007/3-540-61756-6_82
    96 rdf:type schema:CreativeWork
    97 sg:pub.10.1007/3-540-63166-6_16 schema:sameAs https://app.dimensions.ai/details/publication/pub.1037672054
    98 https://doi.org/10.1007/3-540-63166-6_16
    99 rdf:type schema:CreativeWork
    100 sg:pub.10.1007/bf01211087 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008568428
    101 https://doi.org/10.1007/bf01211087
    102 rdf:type schema:CreativeWork
    103 sg:pub.10.1007/bfb0032402 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027875008
    104 https://doi.org/10.1007/bfb0032402
    105 rdf:type schema:CreativeWork
    106 sg:pub.10.1007/bfb0056611 schema:sameAs https://app.dimensions.ai/details/publication/pub.1029972945
    107 https://doi.org/10.1007/bfb0056611
    108 rdf:type schema:CreativeWork
    109 sg:pub.10.1007/bfb0056612 schema:sameAs https://app.dimensions.ai/details/publication/pub.1018243572
    110 https://doi.org/10.1007/bfb0056612
    111 rdf:type schema:CreativeWork
    112 https://doi.org/10.1017/s0956796800000757 schema:sameAs https://app.dimensions.ai/details/publication/pub.1016061186
    113 rdf:type schema:CreativeWork
    114 https://doi.org/10.1017/s0956796800001167 schema:sameAs https://app.dimensions.ai/details/publication/pub.1038404271
    115 rdf:type schema:CreativeWork
    116 https://doi.org/10.1145/136035.136043 schema:sameAs https://app.dimensions.ai/details/publication/pub.1018110957
    117 rdf:type schema:CreativeWork
    118 https://doi.org/10.1145/169683.174155 schema:sameAs https://app.dimensions.ai/details/publication/pub.1022267651
    119 rdf:type schema:CreativeWork
    120 https://doi.org/10.1145/191839.191927 schema:sameAs https://app.dimensions.ai/details/publication/pub.1018675534
    121 rdf:type schema:CreativeWork
    122 https://doi.org/10.1145/242223.242257 schema:sameAs https://app.dimensions.ai/details/publication/pub.1014368099
    123 rdf:type schema:CreativeWork
    124 https://doi.org/10.1145/271510.271525 schema:sameAs https://app.dimensions.ai/details/publication/pub.1037743749
    125 rdf:type schema:CreativeWork
    126 https://doi.org/10.1145/5397.5399 schema:sameAs https://app.dimensions.ai/details/publication/pub.1053218197
    127 rdf:type schema:CreativeWork
    128 https://www.grid.ac/institutes/grid.5254.6 schema:alternateName University of Copenhagen
    129 schema:name DIKU, Department of Computer Science, University of Copenhagen, DK-2100, Copenhagen, Denmark
    130 rdf:type schema:Organization
    131 https://www.grid.ac/institutes/grid.5491.9 schema:alternateName University of Southampton
    132 schema:name Department of Electronics and Computer Science, University of Southampton, SO17 1BJ, Southampton, UK
    133 rdf:type schema:Organization
     




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


    ...