Symbolic Computation via Program Transformation View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2018-10-15

AUTHORS

Henrich Lauko , Petr Ročkai , Jiří Barnat

ABSTRACT

Symbolic computation is an important approach in automated program analysis. Most state-of-the-art tools perform symbolic computation as interpreters and directly maintain symbolic data. In this paper, we show that it is feasible, and in fact practical, to use a compiler-based strategy instead. Using compiler tooling, we propose and implement a transformation which takes a standard program and outputs a program that performs a semantically equivalent, but partially symbolic, computation. The transformed program maintains symbolic values internally and operates directly on them; therefore, the program can be processed by a tool without support for symbolic manipulation.The main motivation for the transformation is in symbolic verification, but there are many other possible use-cases, including test generation and concolic testing. Moreover, using the transformation simplifies tools, since the symbolic computation is handled by the program directly. We have implemented the transformation at the level of LLVM bitcode. The paper includes an experimental evaluation, based on an explicit-state software model checker as a verification backend. More... »

PAGES

313-332

Book

TITLE

Theoretical Aspects of Computing – ICTAC 2018

ISBN

978-3-030-02507-6
978-3-030-02508-3

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-030-02508-3_17

DOI

http://dx.doi.org/10.1007/978-3-030-02508-3_17

DIMENSIONS

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


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/0803", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computer Software", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, 602 00, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, 602 00, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Lauko", 
        "givenName": "Henrich", 
        "id": "sg:person.010156102043.29", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010156102043.29"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, 602 00, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, 602 00, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Ro\u010dkai", 
        "givenName": "Petr", 
        "id": "sg:person.07377571657.86", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, 602 00, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Botanick\u00e1 68a, 602 00, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Barnat", 
        "givenName": "Ji\u0159\u00ed", 
        "id": "sg:person.011367557177.46", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2018-10-15", 
    "datePublishedReg": "2018-10-15", 
    "description": "Symbolic computation is an important approach in automated program analysis. Most state-of-the-art tools perform symbolic computation as interpreters and directly maintain symbolic data. In this paper, we show that it is feasible, and in fact practical, to use a compiler-based strategy instead. Using compiler tooling, we propose and implement a transformation which takes a standard program and outputs a program that performs a semantically equivalent, but partially symbolic, computation. The transformed program maintains symbolic values internally and operates directly on them; therefore, the program can be processed by a tool without support for symbolic manipulation.The main motivation for the transformation is in symbolic verification, but there are many other possible use-cases, including test generation and concolic testing. Moreover, using the transformation simplifies tools, since the symbolic computation is handled by the program directly. We have implemented the transformation at the level of LLVM bitcode. The paper includes an experimental evaluation, based on an explicit-state software model checker as a verification backend.", 
    "editor": [
      {
        "familyName": "Fischer", 
        "givenName": "Bernd", 
        "type": "Person"
      }, 
      {
        "familyName": "Uustalu", 
        "givenName": "Tarmo", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-030-02508-3_17", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-030-02507-6", 
        "978-3-030-02508-3"
      ], 
      "name": "Theoretical Aspects of Computing \u2013 ICTAC 2018", 
      "type": "Book"
    }, 
    "keywords": [
      "software model checkers", 
      "symbolic computation", 
      "compiler-based strategy", 
      "model checker", 
      "symbolic verification", 
      "concolic testing", 
      "symbolic data", 
      "verification backend", 
      "LLVM bitcode", 
      "program analysis", 
      "program transformations", 
      "art tools", 
      "test generation", 
      "experimental evaluation", 
      "symbolic manipulation", 
      "computation", 
      "main motivation", 
      "most states", 
      "important approach", 
      "backend", 
      "checker", 
      "tool", 
      "verification", 
      "interpreters", 
      "tooling", 
      "program", 
      "standard program", 
      "transformation", 
      "data", 
      "support", 
      "symbolic value", 
      "generation", 
      "motivation", 
      "manipulation", 
      "evaluation", 
      "strategies", 
      "testing", 
      "state", 
      "fact", 
      "analysis", 
      "values", 
      "levels", 
      "paper", 
      "approach"
    ], 
    "name": "Symbolic Computation via Program Transformation", 
    "pagination": "313-332", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1107608889"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-030-02508-3_17"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-030-02508-3_17", 
      "https://app.dimensions.ai/details/publication/pub.1107608889"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-08-04T17:16", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220804/entities/gbq_results/chapter/chapter_233.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-030-02508-3_17"
  }
]
 

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/978-3-030-02508-3_17'

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/978-3-030-02508-3_17'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-02508-3_17'

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

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-02508-3_17'


 

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

122 TRIPLES      22 PREDICATES      68 URIs      61 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-030-02508-3_17 schema:about anzsrc-for:08
2 anzsrc-for:0803
3 schema:author N59b62e18251a4aee9123d1912790c747
4 schema:datePublished 2018-10-15
5 schema:datePublishedReg 2018-10-15
6 schema:description Symbolic computation is an important approach in automated program analysis. Most state-of-the-art tools perform symbolic computation as interpreters and directly maintain symbolic data. In this paper, we show that it is feasible, and in fact practical, to use a compiler-based strategy instead. Using compiler tooling, we propose and implement a transformation which takes a standard program and outputs a program that performs a semantically equivalent, but partially symbolic, computation. The transformed program maintains symbolic values internally and operates directly on them; therefore, the program can be processed by a tool without support for symbolic manipulation.The main motivation for the transformation is in symbolic verification, but there are many other possible use-cases, including test generation and concolic testing. Moreover, using the transformation simplifies tools, since the symbolic computation is handled by the program directly. We have implemented the transformation at the level of LLVM bitcode. The paper includes an experimental evaluation, based on an explicit-state software model checker as a verification backend.
7 schema:editor Nd4341dc640e24a5a9ba23e49a99d1558
8 schema:genre chapter
9 schema:isAccessibleForFree true
10 schema:isPartOf Nc891678a4b46459b93b2c9eac894e221
11 schema:keywords LLVM bitcode
12 analysis
13 approach
14 art tools
15 backend
16 checker
17 compiler-based strategy
18 computation
19 concolic testing
20 data
21 evaluation
22 experimental evaluation
23 fact
24 generation
25 important approach
26 interpreters
27 levels
28 main motivation
29 manipulation
30 model checker
31 most states
32 motivation
33 paper
34 program
35 program analysis
36 program transformations
37 software model checkers
38 standard program
39 state
40 strategies
41 support
42 symbolic computation
43 symbolic data
44 symbolic manipulation
45 symbolic value
46 symbolic verification
47 test generation
48 testing
49 tool
50 tooling
51 transformation
52 values
53 verification
54 verification backend
55 schema:name Symbolic Computation via Program Transformation
56 schema:pagination 313-332
57 schema:productId N22e5f88569024514b9b179006c809541
58 N53692d45996042218988afedb46b9a59
59 schema:publisher N2017fb356c744c149f45ce9bc3c06220
60 schema:sameAs https://app.dimensions.ai/details/publication/pub.1107608889
61 https://doi.org/10.1007/978-3-030-02508-3_17
62 schema:sdDatePublished 2022-08-04T17:16
63 schema:sdLicense https://scigraph.springernature.com/explorer/license/
64 schema:sdPublisher N00b3a04ce2c349929a044a352eaafb34
65 schema:url https://doi.org/10.1007/978-3-030-02508-3_17
66 sgo:license sg:explorer/license/
67 sgo:sdDataset chapters
68 rdf:type schema:Chapter
69 N00b3a04ce2c349929a044a352eaafb34 schema:name Springer Nature - SN SciGraph project
70 rdf:type schema:Organization
71 N2017fb356c744c149f45ce9bc3c06220 schema:name Springer Nature
72 rdf:type schema:Organisation
73 N22e5f88569024514b9b179006c809541 schema:name doi
74 schema:value 10.1007/978-3-030-02508-3_17
75 rdf:type schema:PropertyValue
76 N53692d45996042218988afedb46b9a59 schema:name dimensions_id
77 schema:value pub.1107608889
78 rdf:type schema:PropertyValue
79 N59b62e18251a4aee9123d1912790c747 rdf:first sg:person.010156102043.29
80 rdf:rest N9c01bc242fcf42dbaffec68dba5567e5
81 N9c01bc242fcf42dbaffec68dba5567e5 rdf:first sg:person.07377571657.86
82 rdf:rest Nc13052cdbf0c4827ab768f482934db7e
83 Nc13052cdbf0c4827ab768f482934db7e rdf:first sg:person.011367557177.46
84 rdf:rest rdf:nil
85 Nc37963fe922c49f0bf4231d511e61096 schema:familyName Uustalu
86 schema:givenName Tarmo
87 rdf:type schema:Person
88 Nc891678a4b46459b93b2c9eac894e221 schema:isbn 978-3-030-02507-6
89 978-3-030-02508-3
90 schema:name Theoretical Aspects of Computing – ICTAC 2018
91 rdf:type schema:Book
92 Nd4341dc640e24a5a9ba23e49a99d1558 rdf:first Ndde2736736284850ac2d491c7fb399b9
93 rdf:rest Ne71ba914ff0a481cb3e53947c3b49dda
94 Ndde2736736284850ac2d491c7fb399b9 schema:familyName Fischer
95 schema:givenName Bernd
96 rdf:type schema:Person
97 Ne71ba914ff0a481cb3e53947c3b49dda rdf:first Nc37963fe922c49f0bf4231d511e61096
98 rdf:rest rdf:nil
99 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
100 schema:name Information and Computing Sciences
101 rdf:type schema:DefinedTerm
102 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
103 schema:name Computer Software
104 rdf:type schema:DefinedTerm
105 sg:person.010156102043.29 schema:affiliation grid-institutes:grid.10267.32
106 schema:familyName Lauko
107 schema:givenName Henrich
108 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010156102043.29
109 rdf:type schema:Person
110 sg:person.011367557177.46 schema:affiliation grid-institutes:grid.10267.32
111 schema:familyName Barnat
112 schema:givenName Jiří
113 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46
114 rdf:type schema:Person
115 sg:person.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
116 schema:familyName Ročkai
117 schema:givenName Petr
118 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
119 rdf:type schema:Person
120 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Botanická 68a, 602 00, Brno, Czech Republic
121 schema:name Faculty of Informatics, Masaryk University, Botanická 68a, 602 00, Brno, Czech Republic
122 rdf:type schema:Organization
 




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


...