Context-Switch-Directed Verification in DIVINE View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2014

AUTHORS

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

ABSTRACT

In model checking of real-life C and C++ programs, both search efficiency and counterexample readability are very important. In this paper, we suggest context-switch-directed exploration as a way to find a well-readable counterexample faster. Furthermore, we allow to limit the number of context switches used in state-space exploration if desired. The new algorithm is implemented in the DIVINE model checker and enables both unbounded and bounded context-switch-directed exploration for models given in LLVM bitcode, which efficiently allows for verification of multi-threaded C and C++ programs. More... »

PAGES

135-146

Book

TITLE

Mathematical and Engineering Methods in Computer Science

ISBN

978-3-319-14895-3
978-3-319-14896-0

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-14896-0_12

DOI

http://dx.doi.org/10.1007/978-3-319-14896-0_12

DIMENSIONS

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


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"
      }
    ], 
    "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": "\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": "2014", 
    "datePublishedReg": "2014-01-01", 
    "description": "In model checking of real-life C and C++ programs, both search efficiency and counterexample readability are very important. In this paper, we suggest context-switch-directed exploration as a way to find a well-readable counterexample faster. Furthermore, we allow to limit the number of context switches used in state-space exploration if desired. The new algorithm is implemented in the DIVINE model checker and enables both unbounded and bounded context-switch-directed exploration for models given in LLVM bitcode, which efficiently allows for verification of multi-threaded C and C++ programs.", 
    "editor": [
      {
        "familyName": "Hlin\u011bn\u00fd", 
        "givenName": "Petr", 
        "type": "Person"
      }, 
      {
        "familyName": "Dvo\u0159\u00e1k", 
        "givenName": "Zden\u011bk", 
        "type": "Person"
      }, 
      {
        "familyName": "Jaro\u0161", 
        "givenName": "Ji\u0159\u00ed", 
        "type": "Person"
      }, 
      {
        "familyName": "Kofro\u0148", 
        "givenName": "Jan", 
        "type": "Person"
      }, 
      {
        "familyName": "Ko\u0159enek", 
        "givenName": "Jan", 
        "type": "Person"
      }, 
      {
        "familyName": "Matula", 
        "givenName": "Petr", 
        "type": "Person"
      }, 
      {
        "familyName": "Pala", 
        "givenName": "Karel", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-14896-0_12", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-319-14895-3", 
        "978-3-319-14896-0"
      ], 
      "name": "Mathematical and Engineering Methods in Computer Science", 
      "type": "Book"
    }, 
    "keywords": [
      "context switches", 
      "DIVINE model checker", 
      "state space exploration", 
      "model checker", 
      "model checking", 
      "search efficiency", 
      "LLVM bitcode", 
      "new algorithm", 
      "verification", 
      "checker", 
      "checking", 
      "algorithm", 
      "exploration", 
      "readability", 
      "efficiency", 
      "program", 
      "way", 
      "counterexamples", 
      "model", 
      "number", 
      "switch", 
      "divine", 
      "paper"
    ], 
    "name": "Context-Switch-Directed Verification in DIVINE", 
    "pagination": "135-146", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1048082518"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-14896-0_12"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-14896-0_12", 
      "https://app.dimensions.ai/details/publication/pub.1048082518"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-08-04T17:20", 
    "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_406.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-14896-0_12"
  }
]
 

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-14896-0_12'

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-14896-0_12'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-14896-0_12'

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-14896-0_12'


 

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

126 TRIPLES      22 PREDICATES      48 URIs      41 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-14896-0_12 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N22f0ebdfe0344e92949db3f0909f781e
4 schema:datePublished 2014
5 schema:datePublishedReg 2014-01-01
6 schema:description In model checking of real-life C and C++ programs, both search efficiency and counterexample readability are very important. In this paper, we suggest context-switch-directed exploration as a way to find a well-readable counterexample faster. Furthermore, we allow to limit the number of context switches used in state-space exploration if desired. The new algorithm is implemented in the DIVINE model checker and enables both unbounded and bounded context-switch-directed exploration for models given in LLVM bitcode, which efficiently allows for verification of multi-threaded C and C++ programs.
7 schema:editor Nb6c6286443a04c878587140657da5252
8 schema:genre chapter
9 schema:isAccessibleForFree false
10 schema:isPartOf Nada1d8494ac2437e941f665bb71e11cb
11 schema:keywords DIVINE model checker
12 LLVM bitcode
13 algorithm
14 checker
15 checking
16 context switches
17 counterexamples
18 divine
19 efficiency
20 exploration
21 model
22 model checker
23 model checking
24 new algorithm
25 number
26 paper
27 program
28 readability
29 search efficiency
30 state space exploration
31 switch
32 verification
33 way
34 schema:name Context-Switch-Directed Verification in DIVINE
35 schema:pagination 135-146
36 schema:productId N2f8a35005c74421bbb836f9ce8fd6b7f
37 Nc5dd55ef664a471d9bd6a79c67c78c12
38 schema:publisher N4852902a45754ac4a43b5e04acc32038
39 schema:sameAs https://app.dimensions.ai/details/publication/pub.1048082518
40 https://doi.org/10.1007/978-3-319-14896-0_12
41 schema:sdDatePublished 2022-08-04T17:20
42 schema:sdLicense https://scigraph.springernature.com/explorer/license/
43 schema:sdPublisher Nd9059be9871a416db643941a935e0307
44 schema:url https://doi.org/10.1007/978-3-319-14896-0_12
45 sgo:license sg:explorer/license/
46 sgo:sdDataset chapters
47 rdf:type schema:Chapter
48 N22f0ebdfe0344e92949db3f0909f781e rdf:first sg:person.016057731543.01
49 rdf:rest Na328d99540444e36a866ea3b4650edea
50 N2f8a35005c74421bbb836f9ce8fd6b7f schema:name dimensions_id
51 schema:value pub.1048082518
52 rdf:type schema:PropertyValue
53 N4852902a45754ac4a43b5e04acc32038 schema:name Springer Nature
54 rdf:type schema:Organisation
55 N6fa936a2a57645479cd63b07650f2e1c schema:familyName Matula
56 schema:givenName Petr
57 rdf:type schema:Person
58 N907676e76a48406588b2df67e99cf247 rdf:first Ne507e3e8765642dea87782da88bef1ec
59 rdf:rest N97de9ec38bd14003a8b74a084e2cc8ad
60 N97de9ec38bd14003a8b74a084e2cc8ad rdf:first N6fa936a2a57645479cd63b07650f2e1c
61 rdf:rest Neeb588cbc7dd4176a00a0d57ebd654e7
62 Na328d99540444e36a866ea3b4650edea rdf:first sg:person.07377571657.86
63 rdf:rest Ne30c514528af4ca1ab4454b04ac8f256
64 Nada1d8494ac2437e941f665bb71e11cb schema:isbn 978-3-319-14895-3
65 978-3-319-14896-0
66 schema:name Mathematical and Engineering Methods in Computer Science
67 rdf:type schema:Book
68 Nb6c6286443a04c878587140657da5252 rdf:first Nf7ed03a189574163863e9ab78ec77476
69 rdf:rest Ne4d13d6b203446f09f43b4a54fa4cdff
70 Nc089fb29b04b4de0bea2da3e5478bcb6 schema:familyName Jaroš
71 schema:givenName Jiří
72 rdf:type schema:Person
73 Nc5dd55ef664a471d9bd6a79c67c78c12 schema:name doi
74 schema:value 10.1007/978-3-319-14896-0_12
75 rdf:type schema:PropertyValue
76 Nd326613abae44bd4bf548b219164bc06 schema:familyName Pala
77 schema:givenName Karel
78 rdf:type schema:Person
79 Nd9059be9871a416db643941a935e0307 schema:name Springer Nature - SN SciGraph project
80 rdf:type schema:Organization
81 Ndbfee988b8ff49039968142afe222287 rdf:first Nf1a4d36213f742a59fc8fa7bd08263c3
82 rdf:rest N907676e76a48406588b2df67e99cf247
83 Ndc5a669d3c824544a4b5a87cf9fbe7f2 schema:familyName Dvořák
84 schema:givenName Zdeněk
85 rdf:type schema:Person
86 Ne30c514528af4ca1ab4454b04ac8f256 rdf:first sg:person.011367557177.46
87 rdf:rest rdf:nil
88 Ne4d13d6b203446f09f43b4a54fa4cdff rdf:first Ndc5a669d3c824544a4b5a87cf9fbe7f2
89 rdf:rest Ne98a1990a7ed4c9a98dc603bd0dea1fc
90 Ne507e3e8765642dea87782da88bef1ec schema:familyName Kořenek
91 schema:givenName Jan
92 rdf:type schema:Person
93 Ne98a1990a7ed4c9a98dc603bd0dea1fc rdf:first Nc089fb29b04b4de0bea2da3e5478bcb6
94 rdf:rest Ndbfee988b8ff49039968142afe222287
95 Neeb588cbc7dd4176a00a0d57ebd654e7 rdf:first Nd326613abae44bd4bf548b219164bc06
96 rdf:rest rdf:nil
97 Nf1a4d36213f742a59fc8fa7bd08263c3 schema:familyName Kofroň
98 schema:givenName Jan
99 rdf:type schema:Person
100 Nf7ed03a189574163863e9ab78ec77476 schema:familyName Hliněný
101 schema:givenName Petr
102 rdf:type schema:Person
103 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
104 schema:name Information and Computing Sciences
105 rdf:type schema:DefinedTerm
106 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
107 schema:name Computation Theory and Mathematics
108 rdf:type schema:DefinedTerm
109 sg:person.011367557177.46 schema:affiliation grid-institutes:grid.10267.32
110 schema:familyName Barnat
111 schema:givenName Jiří
112 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46
113 rdf:type schema:Person
114 sg:person.016057731543.01 schema:affiliation grid-institutes:grid.10267.32
115 schema:familyName Štill
116 schema:givenName Vladimír
117 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016057731543.01
118 rdf:type schema:Person
119 sg:person.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
120 schema:familyName Ročkai
121 schema:givenName Petr
122 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
123 rdf:type schema:Person
124 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
125 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
126 rdf:type schema:Organization
 




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


...