Techniques for Memory-Efficient Model Checking of C and C++ Code View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2015-08-21

AUTHORS

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

ABSTRACT

We present an overview of techniques that, in combination, lead to a memory-efficient implementation of a model checker for LLVM bitcode, suitable for verification of realistic C and C++ programs.As a central component, we present the design of a tree compression scheme and evaluate the implementation in context of explicit-state safety, LTL and untimed-LTL (for timed automata) model checking. Our design is characterised by dynamic, multi-way adaptive partitioning of state vectors for efficient storage in a tree-compressed hash table, representing the closed set in the model checking algorithm. To complement the tree compression technique, we present a special-purpose memory allocation algorithm with very compact memory layout and negligible performance penalty. More... »

PAGES

268-282

Book

TITLE

Software Engineering and Formal Methods

ISBN

978-3-319-22968-3
978-3-319-22969-0

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-22969-0_19

DOI

http://dx.doi.org/10.1007/978-3-319-22969-0_19

DIMENSIONS

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


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": "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": "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": "2015-08-21", 
    "datePublishedReg": "2015-08-21", 
    "description": "We present an overview of techniques that, in combination, lead to a memory-efficient implementation of a model checker for LLVM bitcode, suitable for verification of realistic C and C++ programs.As a central component, we present the design of a tree compression scheme and evaluate the implementation in context of explicit-state safety, LTL and untimed-LTL (for timed automata) model checking. Our design is characterised by dynamic, multi-way adaptive partitioning of state vectors for efficient storage in a tree-compressed hash table, representing the closed set in the model checking algorithm. To complement the tree compression technique, we present a special-purpose memory allocation algorithm with very compact memory layout and negligible performance penalty.", 
    "editor": [
      {
        "familyName": "Calinescu", 
        "givenName": "Radu", 
        "type": "Person"
      }, 
      {
        "familyName": "Rumpe", 
        "givenName": "Bernhard", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-22969-0_19", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-319-22968-3", 
        "978-3-319-22969-0"
      ], 
      "name": "Software Engineering and Formal Methods", 
      "type": "Book"
    }, 
    "keywords": [
      "model checking", 
      "model checking algorithm", 
      "memory-efficient implementation", 
      "negligible performance penalty", 
      "model checker", 
      "hash table", 
      "compression scheme", 
      "memory layout", 
      "memory allocation", 
      "compression techniques", 
      "LLVM bitcode", 
      "checking algorithm", 
      "efficient storage", 
      "adaptive partitioning", 
      "performance penalty", 
      "overview of techniques", 
      "checking", 
      "implementation", 
      "checker", 
      "algorithm", 
      "technique", 
      "verification", 
      "LTL", 
      "code", 
      "design", 
      "scheme", 
      "state vector", 
      "allocation", 
      "layout", 
      "set", 
      "partitioning", 
      "table", 
      "central component", 
      "storage", 
      "closed set", 
      "vector", 
      "penalty", 
      "context", 
      "overview", 
      "program", 
      "components", 
      "safety", 
      "combination"
    ], 
    "name": "Techniques for Memory-Efficient Model Checking of C and C++ Code", 
    "pagination": "268-282", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1017674659"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-22969-0_19"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-22969-0_19", 
      "https://app.dimensions.ai/details/publication/pub.1017674659"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-08-04T17:17", 
    "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_261.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-22969-0_19"
  }
]
 

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-22969-0_19'

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-22969-0_19'

Turtle is a human-readable linked data format.

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

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-22969-0_19'


 

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

121 TRIPLES      22 PREDICATES      67 URIs      60 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-22969-0_19 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author Ne71a248fd21c4a818bfd2c1d2638bd4a
4 schema:datePublished 2015-08-21
5 schema:datePublishedReg 2015-08-21
6 schema:description We present an overview of techniques that, in combination, lead to a memory-efficient implementation of a model checker for LLVM bitcode, suitable for verification of realistic C and C++ programs.As a central component, we present the design of a tree compression scheme and evaluate the implementation in context of explicit-state safety, LTL and untimed-LTL (for timed automata) model checking. Our design is characterised by dynamic, multi-way adaptive partitioning of state vectors for efficient storage in a tree-compressed hash table, representing the closed set in the model checking algorithm. To complement the tree compression technique, we present a special-purpose memory allocation algorithm with very compact memory layout and negligible performance penalty.
7 schema:editor N3882166e0d41422c840c200129db5e45
8 schema:genre chapter
9 schema:isAccessibleForFree false
10 schema:isPartOf Nc01d0560cd1e4ac4a2bf489cc7430a58
11 schema:keywords LLVM bitcode
12 LTL
13 adaptive partitioning
14 algorithm
15 allocation
16 central component
17 checker
18 checking
19 checking algorithm
20 closed set
21 code
22 combination
23 components
24 compression scheme
25 compression techniques
26 context
27 design
28 efficient storage
29 hash table
30 implementation
31 layout
32 memory allocation
33 memory layout
34 memory-efficient implementation
35 model checker
36 model checking
37 model checking algorithm
38 negligible performance penalty
39 overview
40 overview of techniques
41 partitioning
42 penalty
43 performance penalty
44 program
45 safety
46 scheme
47 set
48 state vector
49 storage
50 table
51 technique
52 vector
53 verification
54 schema:name Techniques for Memory-Efficient Model Checking of C and C++ Code
55 schema:pagination 268-282
56 schema:productId N58a9757722f94e2692b1ae10c9629a59
57 N81cc559bb96e4a1686030d1b187caf06
58 schema:publisher Na5776541cc6043f9b2f237a1b44451d6
59 schema:sameAs https://app.dimensions.ai/details/publication/pub.1017674659
60 https://doi.org/10.1007/978-3-319-22969-0_19
61 schema:sdDatePublished 2022-08-04T17:17
62 schema:sdLicense https://scigraph.springernature.com/explorer/license/
63 schema:sdPublisher Na049bf7e6e074c6d8ea4444002421934
64 schema:url https://doi.org/10.1007/978-3-319-22969-0_19
65 sgo:license sg:explorer/license/
66 sgo:sdDataset chapters
67 rdf:type schema:Chapter
68 N2ab4c881f8e34e2b8ca2e8f98a08bc1e rdf:first sg:person.011367557177.46
69 rdf:rest rdf:nil
70 N3882166e0d41422c840c200129db5e45 rdf:first N5f5bcb70ffe34016af464d4c1100e2c2
71 rdf:rest N74e01ca54f7d41f383152259d883c9f5
72 N469a6eff123f408d87464020ce5c78c2 rdf:first sg:person.016057731543.01
73 rdf:rest N2ab4c881f8e34e2b8ca2e8f98a08bc1e
74 N58a9757722f94e2692b1ae10c9629a59 schema:name doi
75 schema:value 10.1007/978-3-319-22969-0_19
76 rdf:type schema:PropertyValue
77 N5f5bcb70ffe34016af464d4c1100e2c2 schema:familyName Calinescu
78 schema:givenName Radu
79 rdf:type schema:Person
80 N64c51a546e724a0cb22bd1c75d1b2f60 schema:familyName Rumpe
81 schema:givenName Bernhard
82 rdf:type schema:Person
83 N74e01ca54f7d41f383152259d883c9f5 rdf:first N64c51a546e724a0cb22bd1c75d1b2f60
84 rdf:rest rdf:nil
85 N81cc559bb96e4a1686030d1b187caf06 schema:name dimensions_id
86 schema:value pub.1017674659
87 rdf:type schema:PropertyValue
88 Na049bf7e6e074c6d8ea4444002421934 schema:name Springer Nature - SN SciGraph project
89 rdf:type schema:Organization
90 Na5776541cc6043f9b2f237a1b44451d6 schema:name Springer Nature
91 rdf:type schema:Organisation
92 Nc01d0560cd1e4ac4a2bf489cc7430a58 schema:isbn 978-3-319-22968-3
93 978-3-319-22969-0
94 schema:name Software Engineering and Formal Methods
95 rdf:type schema:Book
96 Ne71a248fd21c4a818bfd2c1d2638bd4a rdf:first sg:person.07377571657.86
97 rdf:rest N469a6eff123f408d87464020ce5c78c2
98 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
99 schema:name Information and Computing Sciences
100 rdf:type schema:DefinedTerm
101 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
102 schema:name Computation Theory and Mathematics
103 rdf:type schema:DefinedTerm
104 sg:person.011367557177.46 schema:affiliation grid-institutes:grid.10267.32
105 schema:familyName Barnat
106 schema:givenName Jiří
107 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46
108 rdf:type schema:Person
109 sg:person.016057731543.01 schema:affiliation grid-institutes:grid.10267.32
110 schema:familyName Štill
111 schema:givenName Vladimír
112 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016057731543.01
113 rdf:type schema:Person
114 sg:person.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
115 schema:familyName Ročkai
116 schema:givenName Petr
117 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
118 rdf:type schema:Person
119 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
120 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
121 rdf:type schema:Organization
 




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


...