Model Checking of C and C++ with DIVINE 4 View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2017-09-27

AUTHORS

Zuzana Baranová , Jiří Barnat , Katarína Kejstová , Tadeáš Kučera , Henrich Lauko , Jan Mrázek , Petr Ročkai , Vladimír Štill

ABSTRACT

The fourth version of the DIVINE model checker provides a modular platform for verification of real-world programs. It is built around an efficient interpreter of LLVM code which, together with a small, verification-oriented operating system and a set of runtime libraries, enables verification of code written in C and C++.

PAGES

201-207

Book

TITLE

Automated Technology for Verification and Analysis

ISBN

978-3-319-68166-5
978-3-319-68167-2

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-68167-2_14

DOI

http://dx.doi.org/10.1007/978-3-319-68167-2_14

DIMENSIONS

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


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": "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": "Baranov\u00e1", 
        "givenName": "Zuzana", 
        "id": "sg:person.015764046444.46", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015764046444.46"
        ], 
        "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"
      }, 
      {
        "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": "Kejstov\u00e1", 
        "givenName": "Katar\u00edna", 
        "id": "sg:person.07560316405.30", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07560316405.30"
        ], 
        "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": "Ku\u010dera", 
        "givenName": "Tade\u00e1\u0161", 
        "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": "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": "Mr\u00e1zek", 
        "givenName": "Jan", 
        "id": "sg:person.011477066543.53", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011477066543.53"
        ], 
        "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": "\u0160till", 
        "givenName": "Vladim\u00edr", 
        "id": "sg:person.016057731543.01", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016057731543.01"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2017-09-27", 
    "datePublishedReg": "2017-09-27", 
    "description": "The fourth version of the DIVINE model checker provides a modular platform for verification of real-world programs. It is built around an efficient interpreter of LLVM code which, together with a small, verification-oriented operating system and a set of runtime libraries, enables verification of code written in C and C++.", 
    "editor": [
      {
        "familyName": "D'Souza", 
        "givenName": "Deepak", 
        "type": "Person"
      }, 
      {
        "familyName": "Narayan Kumar", 
        "givenName": "K.", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-68167-2_14", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-319-68166-5", 
        "978-3-319-68167-2"
      ], 
      "name": "Automated Technology for Verification and Analysis", 
      "type": "Book"
    }, 
    "keywords": [
      "DIVINE model checker", 
      "real-world programs", 
      "verification of codes", 
      "runtime library", 
      "model checker", 
      "operating system", 
      "LLVM code", 
      "model checking", 
      "efficient interpreters", 
      "modular platform", 
      "verification", 
      "code", 
      "checker", 
      "checking", 
      "platform", 
      "interpreters", 
      "set", 
      "library", 
      "fourth version", 
      "system", 
      "version", 
      "program"
    ], 
    "name": "Model Checking of C and C++ with DIVINE 4", 
    "pagination": "201-207", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1091962613"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-68167-2_14"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-68167-2_14", 
      "https://app.dimensions.ai/details/publication/pub.1091962613"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-08-04T17:21", 
    "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_380.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-68167-2_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-319-68167-2_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-319-68167-2_14'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-68167-2_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-319-68167-2_14'


 

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

138 TRIPLES      22 PREDICATES      47 URIs      39 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-68167-2_14 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 anzsrc-for:0803
4 schema:author N60b5ab33073942ef8efb881d0a861fcc
5 schema:datePublished 2017-09-27
6 schema:datePublishedReg 2017-09-27
7 schema:description The fourth version of the DIVINE model checker provides a modular platform for verification of real-world programs. It is built around an efficient interpreter of LLVM code which, together with a small, verification-oriented operating system and a set of runtime libraries, enables verification of code written in C and C++.
8 schema:editor Nd86825ca81fb4478bad40fabe02e9287
9 schema:genre chapter
10 schema:isAccessibleForFree false
11 schema:isPartOf N78cd27277b9e44c283116229287b160f
12 schema:keywords DIVINE model checker
13 LLVM code
14 checker
15 checking
16 code
17 efficient interpreters
18 fourth version
19 interpreters
20 library
21 model checker
22 model checking
23 modular platform
24 operating system
25 platform
26 program
27 real-world programs
28 runtime library
29 set
30 system
31 verification
32 verification of codes
33 version
34 schema:name Model Checking of C and C++ with DIVINE 4
35 schema:pagination 201-207
36 schema:productId N29aeea653ea241eb8fa314d4dbf26c25
37 Ne9e5d2d36c214629ab2f493ba7fc55e7
38 schema:publisher Naa5f4b7972d943e6983504717270d5ff
39 schema:sameAs https://app.dimensions.ai/details/publication/pub.1091962613
40 https://doi.org/10.1007/978-3-319-68167-2_14
41 schema:sdDatePublished 2022-08-04T17:21
42 schema:sdLicense https://scigraph.springernature.com/explorer/license/
43 schema:sdPublisher N08a5989c010b479ab6c89038e51d7e0b
44 schema:url https://doi.org/10.1007/978-3-319-68167-2_14
45 sgo:license sg:explorer/license/
46 sgo:sdDataset chapters
47 rdf:type schema:Chapter
48 N08a5989c010b479ab6c89038e51d7e0b schema:name Springer Nature - SN SciGraph project
49 rdf:type schema:Organization
50 N1e9dd6b30704412885534665e39eb0d3 rdf:first sg:person.016057731543.01
51 rdf:rest rdf:nil
52 N285c135409c14db6b93f7f95704e1b8e rdf:first sg:person.010156102043.29
53 rdf:rest N5bb5368e2c6e4f12ac3c7f5e84e5159b
54 N29aeea653ea241eb8fa314d4dbf26c25 schema:name doi
55 schema:value 10.1007/978-3-319-68167-2_14
56 rdf:type schema:PropertyValue
57 N38efefe2c8a9494b9946f23f95987136 rdf:first sg:person.07560316405.30
58 rdf:rest N6812f93ea9c543bc8a3a815035e2a73e
59 N3ff3f67a5aaa4b1c8b6dda6e9298791a rdf:first N86ca1e75509b4c02a86133430a69596d
60 rdf:rest rdf:nil
61 N5bb5368e2c6e4f12ac3c7f5e84e5159b rdf:first sg:person.011477066543.53
62 rdf:rest N95db8675a5604e299c3419527c8007c5
63 N60b5ab33073942ef8efb881d0a861fcc rdf:first sg:person.015764046444.46
64 rdf:rest N700d3fd574314cc8a2853ff85946d08b
65 N6812f93ea9c543bc8a3a815035e2a73e rdf:first Nd3d5a496e1d0413e82f15765b81f63e9
66 rdf:rest N285c135409c14db6b93f7f95704e1b8e
67 N700d3fd574314cc8a2853ff85946d08b rdf:first sg:person.011367557177.46
68 rdf:rest N38efefe2c8a9494b9946f23f95987136
69 N78cd27277b9e44c283116229287b160f schema:isbn 978-3-319-68166-5
70 978-3-319-68167-2
71 schema:name Automated Technology for Verification and Analysis
72 rdf:type schema:Book
73 N86ca1e75509b4c02a86133430a69596d schema:familyName Narayan Kumar
74 schema:givenName K.
75 rdf:type schema:Person
76 N95db8675a5604e299c3419527c8007c5 rdf:first sg:person.07377571657.86
77 rdf:rest N1e9dd6b30704412885534665e39eb0d3
78 Naa5f4b7972d943e6983504717270d5ff schema:name Springer Nature
79 rdf:type schema:Organisation
80 Nd3d5a496e1d0413e82f15765b81f63e9 schema:affiliation grid-institutes:grid.10267.32
81 schema:familyName Kučera
82 schema:givenName Tadeáš
83 rdf:type schema:Person
84 Nd725b6ba154f4e42a27a8e2cfefe0923 schema:familyName D'Souza
85 schema:givenName Deepak
86 rdf:type schema:Person
87 Nd86825ca81fb4478bad40fabe02e9287 rdf:first Nd725b6ba154f4e42a27a8e2cfefe0923
88 rdf:rest N3ff3f67a5aaa4b1c8b6dda6e9298791a
89 Ne9e5d2d36c214629ab2f493ba7fc55e7 schema:name dimensions_id
90 schema:value pub.1091962613
91 rdf:type schema:PropertyValue
92 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
93 schema:name Information and Computing Sciences
94 rdf:type schema:DefinedTerm
95 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
96 schema:name Computation Theory and Mathematics
97 rdf:type schema:DefinedTerm
98 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
99 schema:name Computer Software
100 rdf:type schema:DefinedTerm
101 sg:person.010156102043.29 schema:affiliation grid-institutes:grid.10267.32
102 schema:familyName Lauko
103 schema:givenName Henrich
104 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010156102043.29
105 rdf:type schema:Person
106 sg:person.011367557177.46 schema:affiliation grid-institutes:grid.10267.32
107 schema:familyName Barnat
108 schema:givenName Jiří
109 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46
110 rdf:type schema:Person
111 sg:person.011477066543.53 schema:affiliation grid-institutes:grid.10267.32
112 schema:familyName Mrázek
113 schema:givenName Jan
114 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011477066543.53
115 rdf:type schema:Person
116 sg:person.015764046444.46 schema:affiliation grid-institutes:grid.10267.32
117 schema:familyName Baranová
118 schema:givenName Zuzana
119 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015764046444.46
120 rdf:type schema:Person
121 sg:person.016057731543.01 schema:affiliation grid-institutes:grid.10267.32
122 schema:familyName Štill
123 schema:givenName Vladimír
124 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016057731543.01
125 rdf:type schema:Person
126 sg:person.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
127 schema:familyName Ročkai
128 schema:givenName Petr
129 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
130 rdf:type schema:Person
131 sg:person.07560316405.30 schema:affiliation grid-institutes:grid.10267.32
132 schema:familyName Kejstová
133 schema:givenName Katarína
134 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07560316405.30
135 rdf:type schema:Person
136 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
137 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
138 rdf:type schema:Organization
 




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


...