DIVINE: Explicit-State LTL Model Checker View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2016-04-09

AUTHORS

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

ABSTRACT

DIVINE is an LLVM-based LTL model checker that follows the standard automata-based approach to explicit-state model checking. It aims at verification of unmodified parallel C & C++ programs without inputs. To achieve this DIVINE employs several reduction techniques combined with high-performance parallel and distributed computing.

PAGES

920-922

Book

TITLE

Tools and Algorithms for the Construction and Analysis of Systems

ISBN

978-3-662-49673-2
978-3-662-49674-9

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-662-49674-9_60

DOI

http://dx.doi.org/10.1007/978-3-662-49674-9_60

DIMENSIONS

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


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 Universit, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk Universit, 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 Universit, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk Universit, 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 Universit, Brno, Czech Republic", 
          "id": "http://www.grid.ac/institutes/grid.10267.32", 
          "name": [
            "Faculty of Informatics, Masaryk Universit, 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": "2016-04-09", 
    "datePublishedReg": "2016-04-09", 
    "description": "DIVINE is an LLVM-based LTL model checker that follows the standard automata-based approach to explicit-state model checking. It aims at verification of unmodified parallel C & C++ programs without inputs. To achieve this DIVINE employs several reduction techniques combined with high-performance parallel and distributed computing.", 
    "editor": [
      {
        "familyName": "Chechik", 
        "givenName": "Marsha", 
        "type": "Person"
      }, 
      {
        "familyName": "Raskin", 
        "givenName": "Jean-Fran\u00e7ois", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-662-49674-9_60", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-662-49673-2", 
        "978-3-662-49674-9"
      ], 
      "name": "Tools and Algorithms for the Construction and Analysis of Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "LTL model checker", 
      "model checker", 
      "explicit-state model checking", 
      "high performance parallel", 
      "automata-based approach", 
      "model checking", 
      "checker", 
      "reduction techniques", 
      "computing", 
      "LLVM", 
      "checking", 
      "verification", 
      "input", 
      "technique", 
      "parallel", 
      "program", 
      "divine", 
      "approach"
    ], 
    "name": "DIVINE: Explicit-State LTL Model Checker", 
    "pagination": "920-922", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1020029975"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-662-49674-9_60"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-662-49674-9_60", 
      "https://app.dimensions.ai/details/publication/pub.1020029975"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-08-04T17:15", 
    "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_188.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-662-49674-9_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-662-49674-9_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-662-49674-9_60'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-662-49674-9_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-662-49674-9_60'


 

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

100 TRIPLES      22 PREDICATES      43 URIs      35 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-662-49674-9_60 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 anzsrc-for:0803
4 schema:author N41eef389b473468ba03491ae63de6747
5 schema:datePublished 2016-04-09
6 schema:datePublishedReg 2016-04-09
7 schema:description DIVINE is an LLVM-based LTL model checker that follows the standard automata-based approach to explicit-state model checking. It aims at verification of unmodified parallel C & C++ programs without inputs. To achieve this DIVINE employs several reduction techniques combined with high-performance parallel and distributed computing.
8 schema:editor Nb285a18b7f644b6a8f179aa7ec13cd8a
9 schema:genre chapter
10 schema:isAccessibleForFree false
11 schema:isPartOf N6917b088d5224d048b48e6d5b242d9e8
12 schema:keywords LLVM
13 LTL model checker
14 approach
15 automata-based approach
16 checker
17 checking
18 computing
19 divine
20 explicit-state model checking
21 high performance parallel
22 input
23 model checker
24 model checking
25 parallel
26 program
27 reduction techniques
28 technique
29 verification
30 schema:name DIVINE: Explicit-State LTL Model Checker
31 schema:pagination 920-922
32 schema:productId N7bad709f81354898ad1340b7c0a0b009
33 Nb0195590ab78470db2c8998a1ddde522
34 schema:publisher N024926268e1d4d2ba9126500e0be2959
35 schema:sameAs https://app.dimensions.ai/details/publication/pub.1020029975
36 https://doi.org/10.1007/978-3-662-49674-9_60
37 schema:sdDatePublished 2022-08-04T17:15
38 schema:sdLicense https://scigraph.springernature.com/explorer/license/
39 schema:sdPublisher N43b5bfb7983a4a95a2ada29ff80347e3
40 schema:url https://doi.org/10.1007/978-3-662-49674-9_60
41 sgo:license sg:explorer/license/
42 sgo:sdDataset chapters
43 rdf:type schema:Chapter
44 N024926268e1d4d2ba9126500e0be2959 schema:name Springer Nature
45 rdf:type schema:Organisation
46 N10739ec57443470ba0b215f485aa4a96 rdf:first Nb369e16cbf6e4111b882e334717fee12
47 rdf:rest rdf:nil
48 N41eef389b473468ba03491ae63de6747 rdf:first sg:person.016057731543.01
49 rdf:rest N9a259ad6e8e94f41a5920f39536160f3
50 N42a327ec89aa47e0a261be59422b3b47 schema:familyName Chechik
51 schema:givenName Marsha
52 rdf:type schema:Person
53 N43b5bfb7983a4a95a2ada29ff80347e3 schema:name Springer Nature - SN SciGraph project
54 rdf:type schema:Organization
55 N6917b088d5224d048b48e6d5b242d9e8 schema:isbn 978-3-662-49673-2
56 978-3-662-49674-9
57 schema:name Tools and Algorithms for the Construction and Analysis of Systems
58 rdf:type schema:Book
59 N7bad709f81354898ad1340b7c0a0b009 schema:name doi
60 schema:value 10.1007/978-3-662-49674-9_60
61 rdf:type schema:PropertyValue
62 N9a259ad6e8e94f41a5920f39536160f3 rdf:first sg:person.07377571657.86
63 rdf:rest Nb9d1ffd5a89a413e823622aee4f1cc44
64 Nb0195590ab78470db2c8998a1ddde522 schema:name dimensions_id
65 schema:value pub.1020029975
66 rdf:type schema:PropertyValue
67 Nb285a18b7f644b6a8f179aa7ec13cd8a rdf:first N42a327ec89aa47e0a261be59422b3b47
68 rdf:rest N10739ec57443470ba0b215f485aa4a96
69 Nb369e16cbf6e4111b882e334717fee12 schema:familyName Raskin
70 schema:givenName Jean-François
71 rdf:type schema:Person
72 Nb9d1ffd5a89a413e823622aee4f1cc44 rdf:first sg:person.011367557177.46
73 rdf:rest rdf:nil
74 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
75 schema:name Information and Computing Sciences
76 rdf:type schema:DefinedTerm
77 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
78 schema:name Computation Theory and Mathematics
79 rdf:type schema:DefinedTerm
80 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
81 schema:name Computer Software
82 rdf:type schema:DefinedTerm
83 sg:person.011367557177.46 schema:affiliation grid-institutes:grid.10267.32
84 schema:familyName Barnat
85 schema:givenName Jiří
86 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46
87 rdf:type schema:Person
88 sg:person.016057731543.01 schema:affiliation grid-institutes:grid.10267.32
89 schema:familyName Štill
90 schema:givenName Vladimír
91 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016057731543.01
92 rdf:type schema:Person
93 sg:person.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
94 schema:familyName Ročkai
95 schema:givenName Petr
96 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
97 rdf:type schema:Person
98 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk Universit, Brno, Czech Republic
99 schema:name Faculty of Informatics, Masaryk Universit, Brno, Czech Republic
100 rdf:type schema:Organization
 




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


...