Extending DIVINE with Symbolic Verification Using SMT View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2019-04-04

AUTHORS

Henrich Lauko , Vladimír Štill , Petr Ročkai , Jiří Barnat

ABSTRACT

DIVINE is an LLVM-based verification tool focusing on analysis of real-world C and C++ programs. Such programs often interact with their environment, for example via inputs from users or network. When these programs are analyzed, it is desirable that the verification tool can deal with inputs symbolically and analyze runs for all inputs. In DIVINE, it is now possible to deal with input data via symbolic computation instrumented into the original program at the level of LLVM bitcode. Such an instrumented program maintains symbolic values internally and operates directly on them. Instrumentation allows us to enhance the tool with support for symbolic data without substantial modifications of the tool itself. Namely, this competition contribution uses SMT formulae for representation of input data. More... »

PAGES

204-208

Book

TITLE

Tools and Algorithms for the Construction and Analysis of Systems

ISBN

978-3-030-17501-6
978-3-030-17502-3

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-030-17502-3_14

DOI

http://dx.doi.org/10.1007/978-3-030-17502-3_14

DIMENSIONS

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


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, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, 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, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, Brno, Czech Republic"
          ], 
          "type": "Organization"
        }, 
        "familyName": "\u0160till", 
        "givenName": "Vladim\u00edr", 
        "id": "sg:person.016057731543.01", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016057731543.01"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Faculty of Informatics, Masaryk University, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, 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, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk University, 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": "2019-04-04", 
    "datePublishedReg": "2019-04-04", 
    "description": "DIVINE is an LLVM-based verification tool focusing on analysis of real-world C and C++ programs. Such programs often interact with their environment, for example via inputs from users or network. When these programs are analyzed, it is desirable that the verification tool can deal with inputs symbolically and analyze runs for all inputs. In DIVINE, it is now possible to deal with input data via symbolic computation instrumented into the original program at the level of LLVM bitcode. Such an instrumented program maintains symbolic values internally and operates directly on them. Instrumentation allows us to enhance the tool with support for symbolic data without substantial modifications of the tool itself. Namely, this competition contribution uses SMT formulae for representation of input data.", 
    "editor": [
      {
        "familyName": "Beyer", 
        "givenName": "Dirk", 
        "type": "Person"
      }, 
      {
        "familyName": "Huisman", 
        "givenName": "Marieke", 
        "type": "Person"
      }, 
      {
        "familyName": "Kordon", 
        "givenName": "Fabrice", 
        "type": "Person"
      }, 
      {
        "familyName": "Steffen", 
        "givenName": "Bernhard", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-030-17502-3_14", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-030-17501-6", 
        "978-3-030-17502-3"
      ], 
      "name": "Tools and Algorithms for the Construction and Analysis of Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "verification tools", 
      "input data", 
      "symbolic verification", 
      "symbolic data", 
      "instrumented program", 
      "SMT formulas", 
      "LLVM bitcode", 
      "original program", 
      "symbolic computation", 
      "LLVM", 
      "tool", 
      "users", 
      "input", 
      "network", 
      "computation", 
      "verification", 
      "SMT", 
      "representation", 
      "data", 
      "environment", 
      "program", 
      "such programs", 
      "example", 
      "support", 
      "symbolic value", 
      "run", 
      "instrumentation", 
      "contribution", 
      "substantial modification", 
      "analysis", 
      "modification", 
      "formula", 
      "values", 
      "levels", 
      "divine"
    ], 
    "name": "Extending DIVINE with Symbolic Verification Using SMT", 
    "pagination": "204-208", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1113233409"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-030-17502-3_14"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-030-17502-3_14", 
      "https://app.dimensions.ai/details/publication/pub.1113233409"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-08-04T17:13", 
    "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_102.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-030-17502-3_14"
  }
]
 

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-17502-3_14'

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-17502-3_14'

Turtle is a human-readable linked data format.

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

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-17502-3_14'


 

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

130 TRIPLES      22 PREDICATES      59 URIs      52 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-030-17502-3_14 schema:about anzsrc-for:08
2 anzsrc-for:0803
3 schema:author N20d084df88ce47c89a93e417202bdc2f
4 schema:datePublished 2019-04-04
5 schema:datePublishedReg 2019-04-04
6 schema:description DIVINE is an LLVM-based verification tool focusing on analysis of real-world C and C++ programs. Such programs often interact with their environment, for example via inputs from users or network. When these programs are analyzed, it is desirable that the verification tool can deal with inputs symbolically and analyze runs for all inputs. In DIVINE, it is now possible to deal with input data via symbolic computation instrumented into the original program at the level of LLVM bitcode. Such an instrumented program maintains symbolic values internally and operates directly on them. Instrumentation allows us to enhance the tool with support for symbolic data without substantial modifications of the tool itself. Namely, this competition contribution uses SMT formulae for representation of input data.
7 schema:editor Nc8a1d20002c9487d80063cc061370409
8 schema:genre chapter
9 schema:isAccessibleForFree true
10 schema:isPartOf Ne0116642deb54167a516dc03fdb9a905
11 schema:keywords LLVM
12 LLVM bitcode
13 SMT
14 SMT formulas
15 analysis
16 computation
17 contribution
18 data
19 divine
20 environment
21 example
22 formula
23 input
24 input data
25 instrumentation
26 instrumented program
27 levels
28 modification
29 network
30 original program
31 program
32 representation
33 run
34 substantial modification
35 such programs
36 support
37 symbolic computation
38 symbolic data
39 symbolic value
40 symbolic verification
41 tool
42 users
43 values
44 verification
45 verification tools
46 schema:name Extending DIVINE with Symbolic Verification Using SMT
47 schema:pagination 204-208
48 schema:productId N3b27cd1512654e0dbc28d7032283a11b
49 Nb1959792ed8a42e08bcb2b96482a1f42
50 schema:publisher N9c5d3bed50bb4e52929cd6a7ded0e485
51 schema:sameAs https://app.dimensions.ai/details/publication/pub.1113233409
52 https://doi.org/10.1007/978-3-030-17502-3_14
53 schema:sdDatePublished 2022-08-04T17:13
54 schema:sdLicense https://scigraph.springernature.com/explorer/license/
55 schema:sdPublisher Nad3206b21e0d43fca6aedb47d0f8de35
56 schema:url https://doi.org/10.1007/978-3-030-17502-3_14
57 sgo:license sg:explorer/license/
58 sgo:sdDataset chapters
59 rdf:type schema:Chapter
60 N2018bb5d7a4d43afa4ac2ae6ac22f7e2 schema:familyName Beyer
61 schema:givenName Dirk
62 rdf:type schema:Person
63 N20d084df88ce47c89a93e417202bdc2f rdf:first sg:person.010156102043.29
64 rdf:rest N23814fd51f6849ad9c568dad6cfef6b7
65 N23814fd51f6849ad9c568dad6cfef6b7 rdf:first sg:person.016057731543.01
66 rdf:rest N8f9daef5e5b3460f87106d382de2359b
67 N385edbea3ca14505848c725670af4342 rdf:first Ne7d518d842b84af589803c43e4733362
68 rdf:rest rdf:nil
69 N3b27cd1512654e0dbc28d7032283a11b schema:name dimensions_id
70 schema:value pub.1113233409
71 rdf:type schema:PropertyValue
72 N8f9daef5e5b3460f87106d382de2359b rdf:first sg:person.07377571657.86
73 rdf:rest Nb913d416b33a4a7d911d13661ff1f4e0
74 N9c01299bb6e04885aea72ce1ba31f79b rdf:first Nab6f7ec9db0c45fdb70c9ecc5659cfb7
75 rdf:rest N385edbea3ca14505848c725670af4342
76 N9c5d3bed50bb4e52929cd6a7ded0e485 schema:name Springer Nature
77 rdf:type schema:Organisation
78 Nab6f7ec9db0c45fdb70c9ecc5659cfb7 schema:familyName Kordon
79 schema:givenName Fabrice
80 rdf:type schema:Person
81 Nad3206b21e0d43fca6aedb47d0f8de35 schema:name Springer Nature - SN SciGraph project
82 rdf:type schema:Organization
83 Nb1959792ed8a42e08bcb2b96482a1f42 schema:name doi
84 schema:value 10.1007/978-3-030-17502-3_14
85 rdf:type schema:PropertyValue
86 Nb913d416b33a4a7d911d13661ff1f4e0 rdf:first sg:person.011367557177.46
87 rdf:rest rdf:nil
88 Nc70b76fd1b654c3f900af04b47c05980 rdf:first Nc9c31152ed64414587f2983260cce480
89 rdf:rest N9c01299bb6e04885aea72ce1ba31f79b
90 Nc8a1d20002c9487d80063cc061370409 rdf:first N2018bb5d7a4d43afa4ac2ae6ac22f7e2
91 rdf:rest Nc70b76fd1b654c3f900af04b47c05980
92 Nc9c31152ed64414587f2983260cce480 schema:familyName Huisman
93 schema:givenName Marieke
94 rdf:type schema:Person
95 Ne0116642deb54167a516dc03fdb9a905 schema:isbn 978-3-030-17501-6
96 978-3-030-17502-3
97 schema:name Tools and Algorithms for the Construction and Analysis of Systems
98 rdf:type schema:Book
99 Ne7d518d842b84af589803c43e4733362 schema:familyName Steffen
100 schema:givenName Bernhard
101 rdf:type schema:Person
102 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
103 schema:name Information and Computing Sciences
104 rdf:type schema:DefinedTerm
105 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
106 schema:name Computer Software
107 rdf:type schema:DefinedTerm
108 sg:person.010156102043.29 schema:affiliation grid-institutes:grid.10267.32
109 schema:familyName Lauko
110 schema:givenName Henrich
111 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010156102043.29
112 rdf:type schema:Person
113 sg:person.011367557177.46 schema:affiliation grid-institutes:grid.10267.32
114 schema:familyName Barnat
115 schema:givenName Jiří
116 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46
117 rdf:type schema:Person
118 sg:person.016057731543.01 schema:affiliation grid-institutes:grid.10267.32
119 schema:familyName Štill
120 schema:givenName Vladimír
121 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016057731543.01
122 rdf:type schema:Person
123 sg:person.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
124 schema:familyName Ročkai
125 schema:givenName Petr
126 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
127 rdf:type schema:Person
128 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
129 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
130 rdf:type schema:Organization
 




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


...