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

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/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "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/0803", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computer Software", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "DIKU, Department of Computer Science, University of Copenhagen, DK-2100, Copenhagen, Denmark", 
          "id": "http://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": "Department of Electronics and Computer Science, University of Southampton, SO17 1BJ, Southampton, UK", 
          "id": "http://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"
      }
    ], 
    "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"
    }, 
    "keywords": [
      "software verification", 
      "automatic program transformation", 
      "partial deduction", 
      "infinite state space", 
      "model checking", 
      "program transformations", 
      "safety properties", 
      "abstract interpretation", 
      "program inversion", 
      "transformational approach", 
      "finite representation", 
      "state space", 
      "verification", 
      "solution set", 
      "infinite solution sets", 
      "checking", 
      "inverse problem", 
      "deduction", 
      "representation", 
      "set", 
      "space", 
      "transformation", 
      "field", 
      "progress", 
      "recent progress", 
      "interpretation", 
      "inversion", 
      "potential", 
      "properties", 
      "approach", 
      "problem", 
      "Abstraction-based partial deduction", 
      "infinite model checking"
    ], 
    "name": "Abstraction-Based Partial Deduction for Solving Inverse Problems \u2014 A Transformational Approach to Software Verification", 
    "pagination": "93-100", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1008046482"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/3-540-46562-6_8"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/3-540-46562-6_8", 
      "https://app.dimensions.ai/details/publication/pub.1008046482"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-11-01T18:47", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20211101/entities/gbq_results/chapter/chapter_14.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/3-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.

117 TRIPLES      23 PREDICATES      59 URIs      51 LITERALS      7 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 anzsrc-for:0803
4 schema:author Ndaf1171e6092460a8a765066291f3e9c
5 schema:datePublished 2000-01-28
6 schema:datePublishedReg 2000-01-28
7 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.
8 schema:editor N1213814af59f42519c42e185abfa532a
9 schema:genre chapter
10 schema:inLanguage en
11 schema:isAccessibleForFree false
12 schema:isPartOf N1ac4b3a858124317ae283909b6c415cc
13 schema:keywords Abstraction-based partial deduction
14 abstract interpretation
15 approach
16 automatic program transformation
17 checking
18 deduction
19 field
20 finite representation
21 infinite model checking
22 infinite solution sets
23 infinite state space
24 interpretation
25 inverse problem
26 inversion
27 model checking
28 partial deduction
29 potential
30 problem
31 program inversion
32 program transformations
33 progress
34 properties
35 recent progress
36 representation
37 safety properties
38 set
39 software verification
40 solution set
41 space
42 state space
43 transformation
44 transformational approach
45 verification
46 schema:name Abstraction-Based Partial Deduction for Solving Inverse Problems — A Transformational Approach to Software Verification
47 schema:pagination 93-100
48 schema:productId N0f04d02222d141ec873fbb84f3ae6c07
49 N107532ad16a74b468aeb8c0c33f4172b
50 schema:publisher N874f02c3911948d1bd7ece9ef6c753fe
51 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008046482
52 https://doi.org/10.1007/3-540-46562-6_8
53 schema:sdDatePublished 2021-11-01T18:47
54 schema:sdLicense https://scigraph.springernature.com/explorer/license/
55 schema:sdPublisher N02c50e8393a74cc8bcbb78b5c1d0efd9
56 schema:url https://doi.org/10.1007/3-540-46562-6_8
57 sgo:license sg:explorer/license/
58 sgo:sdDataset chapters
59 rdf:type schema:Chapter
60 N02c50e8393a74cc8bcbb78b5c1d0efd9 schema:name Springer Nature - SN SciGraph project
61 rdf:type schema:Organization
62 N0f04d02222d141ec873fbb84f3ae6c07 schema:name dimensions_id
63 schema:value pub.1008046482
64 rdf:type schema:PropertyValue
65 N107532ad16a74b468aeb8c0c33f4172b schema:name doi
66 schema:value 10.1007/3-540-46562-6_8
67 rdf:type schema:PropertyValue
68 N1213814af59f42519c42e185abfa532a rdf:first Naa55db0a2e4a49efa6d9eb90956eeac2
69 rdf:rest N928af34d96d746689493efb3ddbeaad2
70 N19cdf41b18564870a2362f5a4ddbba05 schema:familyName Zamulin
71 schema:givenName Alexandre V.
72 rdf:type schema:Person
73 N1ac4b3a858124317ae283909b6c415cc schema:isbn 978-3-540-46562-1
74 978-3-540-67102-2
75 schema:name Perspectives of System Informatics
76 rdf:type schema:Book
77 N874f02c3911948d1bd7ece9ef6c753fe schema:name Springer Nature
78 rdf:type schema:Organisation
79 N928af34d96d746689493efb3ddbeaad2 rdf:first Ne1296a44350c4061996baf87a5173b57
80 rdf:rest Nc2c14458ca4848b2a26f22658263d8f4
81 Na98f1b1650204b7d8e0c1c774e44519d rdf:first sg:person.011762452312.13
82 rdf:rest rdf:nil
83 Naa55db0a2e4a49efa6d9eb90956eeac2 schema:familyName Bjøner
84 schema:givenName Dines
85 rdf:type schema:Person
86 Nc2c14458ca4848b2a26f22658263d8f4 rdf:first N19cdf41b18564870a2362f5a4ddbba05
87 rdf:rest rdf:nil
88 Ndaf1171e6092460a8a765066291f3e9c rdf:first sg:person.010754010217.31
89 rdf:rest Na98f1b1650204b7d8e0c1c774e44519d
90 Ne1296a44350c4061996baf87a5173b57 schema:familyName Broy
91 schema:givenName Manfred
92 rdf:type schema:Person
93 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
94 schema:name Information and Computing Sciences
95 rdf:type schema:DefinedTerm
96 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
97 schema:name Computation Theory and Mathematics
98 rdf:type schema:DefinedTerm
99 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
100 schema:name Computer Software
101 rdf:type schema:DefinedTerm
102 sg:person.010754010217.31 schema:affiliation grid-institutes:grid.5254.6
103 schema:familyName Glück
104 schema:givenName Robert
105 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010754010217.31
106 rdf:type schema:Person
107 sg:person.011762452312.13 schema:affiliation grid-institutes:grid.5491.9
108 schema:familyName Leuschel
109 schema:givenName Michael
110 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011762452312.13
111 rdf:type schema:Person
112 grid-institutes:grid.5254.6 schema:alternateName DIKU, Department of Computer Science, University of Copenhagen, DK-2100, Copenhagen, Denmark
113 schema:name DIKU, Department of Computer Science, University of Copenhagen, DK-2100, Copenhagen, Denmark
114 rdf:type schema:Organization
115 grid-institutes:grid.5491.9 schema:alternateName Department of Electronics and Computer Science, University of Southampton, SO17 1BJ, Southampton, UK
116 schema:name Department of Electronics and Computer Science, University of Southampton, SO17 1BJ, Southampton, UK
117 rdf:type schema:Organization
 




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


...