DiVinE 3.0 – An Explicit-State Model Checker for Multithreaded C & C++ Programs View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2013

AUTHORS

Jiří Barnat , Luboš Brim , Vojtěch Havel , Jan Havlíček , Jan Kriho , Milan Lenčo , Petr Ročkai , Vladimír Štill , Jiří Weiser

ABSTRACT

We present a new release of the parallel and distributed LTL model checker DiVinE. The major improvement in this new release is an extension of the class of systems that may be verified with the model checker, while preserving the unique DiVinE feature, namely parallel and distributed-memory processing. Version 3.0 comes with support for direct model checking of (closed) multithreaded C/C++ programs, full untimed-LTL model checking of timed automata, and a general-purpose framework for interfacing with arbitrary system modelling tools. More... »

PAGES

863-868

Book

TITLE

Computer Aided Verification

ISBN

978-3-642-39798-1
978-3-642-39799-8

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-39799-8_60

DOI

http://dx.doi.org/10.1007/978-3-642-39799-8_60

DIMENSIONS

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


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": "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": "Brim", 
        "givenName": "Lubo\u0161", 
        "id": "sg:person.0645117057.83", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0645117057.83"
        ], 
        "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": "Havel", 
        "givenName": "Vojt\u011bch", 
        "id": "sg:person.011505107103.14", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011505107103.14"
        ], 
        "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": "Havl\u00ed\u010dek", 
        "givenName": "Jan", 
        "id": "sg:person.0724774500.27", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0724774500.27"
        ], 
        "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": "Kriho", 
        "givenName": "Jan", 
        "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": "Len\u010do", 
        "givenName": "Milan", 
        "id": "sg:person.015325317621.59", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015325317621.59"
        ], 
        "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"
      }, 
      {
        "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": "Weiser", 
        "givenName": "Ji\u0159\u00ed", 
        "id": "sg:person.011734301511.89", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011734301511.89"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2013", 
    "datePublishedReg": "2013-01-01", 
    "description": "We present a new release of the parallel and distributed LTL model checker DiVinE. The major improvement in this new release is an extension of the class of systems that may be verified with the model checker, while preserving the unique DiVinE feature, namely parallel and distributed-memory processing. Version 3.0 comes with support for direct model checking of (closed) multithreaded C/C++ programs, full untimed-LTL model checking of timed automata, and a general-purpose framework for interfacing with arbitrary system modelling tools.", 
    "editor": [
      {
        "familyName": "Sharygina", 
        "givenName": "Natasha", 
        "type": "Person"
      }, 
      {
        "familyName": "Veith", 
        "givenName": "Helmut", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-39799-8_60", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-642-39798-1", 
        "978-3-642-39799-8"
      ], 
      "name": "Computer Aided Verification", 
      "type": "Book"
    }, 
    "keywords": [
      "model checker", 
      "model checking", 
      "general-purpose framework", 
      "LTL model checking", 
      "system modelling tools", 
      "new release", 
      "modelling tools", 
      "checker", 
      "checking", 
      "DiVinE.", 
      "class of systems", 
      "automata", 
      "version 3.0", 
      "framework", 
      "major improvements", 
      "processing", 
      "tool", 
      "system", 
      "features", 
      "extension", 
      "program", 
      "parallel", 
      "support", 
      "class", 
      "improvement", 
      "Explicit", 
      "release", 
      "divine"
    ], 
    "name": "DiVinE 3.0 \u2013 An Explicit-State Model Checker for Multithreaded C & C++ Programs", 
    "pagination": "863-868", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1030844308"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-39799-8_60"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-39799-8_60", 
      "https://app.dimensions.ai/details/publication/pub.1030844308"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-10T10:46", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220509/entities/gbq_results/chapter/chapter_314.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-39799-8_60"
  }
]
 

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-642-39799-8_60'

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-642-39799-8_60'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-39799-8_60'

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-642-39799-8_60'


 

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

148 TRIPLES      23 PREDICATES      54 URIs      47 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-39799-8_60 schema:about anzsrc-for:08
2 anzsrc-for:0803
3 schema:author Nc29f957677e9498288ec14ae5fad8101
4 schema:datePublished 2013
5 schema:datePublishedReg 2013-01-01
6 schema:description We present a new release of the parallel and distributed LTL model checker DiVinE. The major improvement in this new release is an extension of the class of systems that may be verified with the model checker, while preserving the unique DiVinE feature, namely parallel and distributed-memory processing. Version 3.0 comes with support for direct model checking of (closed) multithreaded C/C++ programs, full untimed-LTL model checking of timed automata, and a general-purpose framework for interfacing with arbitrary system modelling tools.
7 schema:editor Nae3971371893484e96edcc229977d538
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N425e93d403124a8c95a0262a6ce37d60
12 schema:keywords DiVinE.
13 Explicit
14 LTL model checking
15 automata
16 checker
17 checking
18 class
19 class of systems
20 divine
21 extension
22 features
23 framework
24 general-purpose framework
25 improvement
26 major improvements
27 model checker
28 model checking
29 modelling tools
30 new release
31 parallel
32 processing
33 program
34 release
35 support
36 system
37 system modelling tools
38 tool
39 version 3.0
40 schema:name DiVinE 3.0 – An Explicit-State Model Checker for Multithreaded C & C++ Programs
41 schema:pagination 863-868
42 schema:productId N970b77cfc8f94fdf9b2921ab7f0c70c9
43 Ne0d7af2e323a4720b2fd5da1f75d2fd8
44 schema:publisher N80a33d3e76a140868b4b91826906662a
45 schema:sameAs https://app.dimensions.ai/details/publication/pub.1030844308
46 https://doi.org/10.1007/978-3-642-39799-8_60
47 schema:sdDatePublished 2022-05-10T10:46
48 schema:sdLicense https://scigraph.springernature.com/explorer/license/
49 schema:sdPublisher N7314b99f7d884ebc903947ae1c504979
50 schema:url https://doi.org/10.1007/978-3-642-39799-8_60
51 sgo:license sg:explorer/license/
52 sgo:sdDataset chapters
53 rdf:type schema:Chapter
54 N098e848085e547c4857b5cbce9330236 rdf:first Nab4d633f076f48d496629a419810e23a
55 rdf:rest Ndee8049fdf4f43b28a2a9590fde2abb9
56 N16ea82ecdc214e609d825837426480b4 rdf:first Nc4f47ad6d644405da0df69180ea83b23
57 rdf:rest rdf:nil
58 N425e93d403124a8c95a0262a6ce37d60 schema:isbn 978-3-642-39798-1
59 978-3-642-39799-8
60 schema:name Computer Aided Verification
61 rdf:type schema:Book
62 N7314b99f7d884ebc903947ae1c504979 schema:name Springer Nature - SN SciGraph project
63 rdf:type schema:Organization
64 N7a58df8219ea4b4595a66f9954dd465b rdf:first sg:person.011734301511.89
65 rdf:rest rdf:nil
66 N7c64116eccb94104b7275b114fec01db rdf:first sg:person.0645117057.83
67 rdf:rest Nabfc940c8738414895d6b6855f58bc35
68 N80a33d3e76a140868b4b91826906662a schema:name Springer Nature
69 rdf:type schema:Organisation
70 N970b77cfc8f94fdf9b2921ab7f0c70c9 schema:name doi
71 schema:value 10.1007/978-3-642-39799-8_60
72 rdf:type schema:PropertyValue
73 Nab4d633f076f48d496629a419810e23a schema:affiliation grid-institutes:grid.10267.32
74 schema:familyName Kriho
75 schema:givenName Jan
76 rdf:type schema:Person
77 Nabfc940c8738414895d6b6855f58bc35 rdf:first sg:person.011505107103.14
78 rdf:rest Nbedfa75a11a9433ebe3240c337988c01
79 Nae3971371893484e96edcc229977d538 rdf:first Nc2a8ee55716a464cabd168df14de3295
80 rdf:rest N16ea82ecdc214e609d825837426480b4
81 Nbedfa75a11a9433ebe3240c337988c01 rdf:first sg:person.0724774500.27
82 rdf:rest N098e848085e547c4857b5cbce9330236
83 Nc29f957677e9498288ec14ae5fad8101 rdf:first sg:person.011367557177.46
84 rdf:rest N7c64116eccb94104b7275b114fec01db
85 Nc2a8ee55716a464cabd168df14de3295 schema:familyName Sharygina
86 schema:givenName Natasha
87 rdf:type schema:Person
88 Nc4f47ad6d644405da0df69180ea83b23 schema:familyName Veith
89 schema:givenName Helmut
90 rdf:type schema:Person
91 Nda2da8793029476883a13e9544eb9d98 rdf:first sg:person.016057731543.01
92 rdf:rest N7a58df8219ea4b4595a66f9954dd465b
93 Ndb41977bb1de4380ad2261b34975a55b rdf:first sg:person.07377571657.86
94 rdf:rest Nda2da8793029476883a13e9544eb9d98
95 Ndee8049fdf4f43b28a2a9590fde2abb9 rdf:first sg:person.015325317621.59
96 rdf:rest Ndb41977bb1de4380ad2261b34975a55b
97 Ne0d7af2e323a4720b2fd5da1f75d2fd8 schema:name dimensions_id
98 schema:value pub.1030844308
99 rdf:type schema:PropertyValue
100 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
101 schema:name Information and Computing Sciences
102 rdf:type schema:DefinedTerm
103 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
104 schema:name Computer Software
105 rdf:type schema:DefinedTerm
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.011505107103.14 schema:affiliation grid-institutes:grid.10267.32
112 schema:familyName Havel
113 schema:givenName Vojtěch
114 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011505107103.14
115 rdf:type schema:Person
116 sg:person.011734301511.89 schema:affiliation grid-institutes:grid.10267.32
117 schema:familyName Weiser
118 schema:givenName Jiří
119 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011734301511.89
120 rdf:type schema:Person
121 sg:person.015325317621.59 schema:affiliation grid-institutes:grid.10267.32
122 schema:familyName Lenčo
123 schema:givenName Milan
124 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015325317621.59
125 rdf:type schema:Person
126 sg:person.016057731543.01 schema:affiliation grid-institutes:grid.10267.32
127 schema:familyName Štill
128 schema:givenName Vladimír
129 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016057731543.01
130 rdf:type schema:Person
131 sg:person.0645117057.83 schema:affiliation grid-institutes:grid.10267.32
132 schema:familyName Brim
133 schema:givenName Luboš
134 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0645117057.83
135 rdf:type schema:Person
136 sg:person.0724774500.27 schema:affiliation grid-institutes:grid.10267.32
137 schema:familyName Havlíček
138 schema:givenName Jan
139 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0724774500.27
140 rdf:type schema:Person
141 sg:person.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
142 schema:familyName Ročkai
143 schema:givenName Petr
144 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
145 rdf:type schema:Person
146 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
147 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
148 rdf:type schema:Organization
 




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


...