Improved State Space Reductions for LTL Model Checking of C and C++ Programs View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2013

AUTHORS

Petr Ročkai , Jiří Barnat , Luboš Brim

ABSTRACT

In this paper, we present substantial improvements in efficiency of explicit-state LTL model checking of C & C++ programs, building on [2], including improvements to state representation and to state space reduction techniques. The improved state representation allows to easily exploit symmetries in heap configurations of the program, especially in programs with interleaved heap allocations. Finally, we present a major improvement through a semi-dynamic proviso for partial-order reduction, based on eager local searches constrained through control-flow loop detection. More... »

PAGES

1-15

Book

TITLE

NASA Formal Methods

ISBN

978-3-642-38087-7
978-3-642-38088-4

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-38088-4_1

DOI

http://dx.doi.org/10.1007/978-3-642-38088-4_1

DIMENSIONS

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


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": "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"
      }
    ], 
    "datePublished": "2013", 
    "datePublishedReg": "2013-01-01", 
    "description": "In this paper, we present substantial improvements in efficiency of explicit-state LTL model checking of C & C++ programs, building on [2], including improvements to state representation and to state space reduction techniques. The improved state representation allows to easily exploit symmetries in heap configurations of the program, especially in programs with interleaved heap allocations. Finally, we present a major improvement through a semi-dynamic proviso for partial-order reduction, based on eager local searches constrained through control-flow loop detection.", 
    "editor": [
      {
        "familyName": "Brat", 
        "givenName": "Guillaume", 
        "type": "Person"
      }, 
      {
        "familyName": "Rungta", 
        "givenName": "Neha", 
        "type": "Person"
      }, 
      {
        "familyName": "Venet", 
        "givenName": "Arnaud", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-38088-4_1", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-642-38087-7", 
        "978-3-642-38088-4"
      ], 
      "name": "NASA Formal Methods", 
      "type": "Book"
    }, 
    "keywords": [
      "reduction techniques", 
      "loop detection", 
      "substantial improvement", 
      "major improvements", 
      "space reduction", 
      "efficiency", 
      "configuration", 
      "improvement", 
      "reduction", 
      "technique", 
      "state representation", 
      "detection", 
      "representation", 
      "local search", 
      "checking", 
      "program", 
      "symmetry", 
      "state space reduction techniques", 
      "allocation", 
      "state space reduction", 
      "proviso", 
      "model checking", 
      "partial order reduction", 
      "search", 
      "LTL model checking", 
      "heap allocation", 
      "paper"
    ], 
    "name": "Improved State Space Reductions for LTL Model Checking of C and C++ Programs", 
    "pagination": "1-15", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1038878134"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-38088-4_1"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-38088-4_1", 
      "https://app.dimensions.ai/details/publication/pub.1038878134"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-05-20T07:47", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220519/entities/gbq_results/chapter/chapter_398.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-642-38088-4_1"
  }
]
 

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-38088-4_1'

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-38088-4_1'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-38088-4_1'

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-38088-4_1'


 

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

111 TRIPLES      23 PREDICATES      53 URIs      46 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-38088-4_1 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author Na1c9e28c8be245a8bf61554826649976
4 schema:datePublished 2013
5 schema:datePublishedReg 2013-01-01
6 schema:description In this paper, we present substantial improvements in efficiency of explicit-state LTL model checking of C & C++ programs, building on [2], including improvements to state representation and to state space reduction techniques. The improved state representation allows to easily exploit symmetries in heap configurations of the program, especially in programs with interleaved heap allocations. Finally, we present a major improvement through a semi-dynamic proviso for partial-order reduction, based on eager local searches constrained through control-flow loop detection.
7 schema:editor N6c88b292843f4ace9e0d7cac5b1dff17
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf N5632ac8fe623450eb158400af11113fe
12 schema:keywords LTL model checking
13 allocation
14 checking
15 configuration
16 detection
17 efficiency
18 heap allocation
19 improvement
20 local search
21 loop detection
22 major improvements
23 model checking
24 paper
25 partial order reduction
26 program
27 proviso
28 reduction
29 reduction techniques
30 representation
31 search
32 space reduction
33 state representation
34 state space reduction
35 state space reduction techniques
36 substantial improvement
37 symmetry
38 technique
39 schema:name Improved State Space Reductions for LTL Model Checking of C and C++ Programs
40 schema:pagination 1-15
41 schema:productId N020b00e876c148be9713d0e8301a63db
42 Nfed5b3e79b444bc194b8bc26025dccf3
43 schema:publisher Nf18608a8aacc47899e2033ad02795f1d
44 schema:sameAs https://app.dimensions.ai/details/publication/pub.1038878134
45 https://doi.org/10.1007/978-3-642-38088-4_1
46 schema:sdDatePublished 2022-05-20T07:47
47 schema:sdLicense https://scigraph.springernature.com/explorer/license/
48 schema:sdPublisher N3f714b33045d4446a58a4043461b9ddc
49 schema:url https://doi.org/10.1007/978-3-642-38088-4_1
50 sgo:license sg:explorer/license/
51 sgo:sdDataset chapters
52 rdf:type schema:Chapter
53 N020b00e876c148be9713d0e8301a63db schema:name dimensions_id
54 schema:value pub.1038878134
55 rdf:type schema:PropertyValue
56 N3f714b33045d4446a58a4043461b9ddc schema:name Springer Nature - SN SciGraph project
57 rdf:type schema:Organization
58 N5632ac8fe623450eb158400af11113fe schema:isbn 978-3-642-38087-7
59 978-3-642-38088-4
60 schema:name NASA Formal Methods
61 rdf:type schema:Book
62 N59eada226991433e94c51d4043c77af4 rdf:first Naff44a2b2fab4f52988ffa7d01874b25
63 rdf:rest N5c3747a10ba5445da5e7632eb0c36f6f
64 N5c3747a10ba5445da5e7632eb0c36f6f rdf:first Na263528e5267447f96ee5499ed906b70
65 rdf:rest rdf:nil
66 N6659cf91b5f04e2b8a6b47f433765eee schema:familyName Brat
67 schema:givenName Guillaume
68 rdf:type schema:Person
69 N6c88b292843f4ace9e0d7cac5b1dff17 rdf:first N6659cf91b5f04e2b8a6b47f433765eee
70 rdf:rest N59eada226991433e94c51d4043c77af4
71 Na1c9e28c8be245a8bf61554826649976 rdf:first sg:person.07377571657.86
72 rdf:rest Na5bf0fc0a427433fb2a9e02073fc8fcb
73 Na263528e5267447f96ee5499ed906b70 schema:familyName Venet
74 schema:givenName Arnaud
75 rdf:type schema:Person
76 Na5bf0fc0a427433fb2a9e02073fc8fcb rdf:first sg:person.011367557177.46
77 rdf:rest Nf59aaa28d2414e7f8c326192cb5074c9
78 Naff44a2b2fab4f52988ffa7d01874b25 schema:familyName Rungta
79 schema:givenName Neha
80 rdf:type schema:Person
81 Nf18608a8aacc47899e2033ad02795f1d schema:name Springer Nature
82 rdf:type schema:Organisation
83 Nf59aaa28d2414e7f8c326192cb5074c9 rdf:first sg:person.0645117057.83
84 rdf:rest rdf:nil
85 Nfed5b3e79b444bc194b8bc26025dccf3 schema:name doi
86 schema:value 10.1007/978-3-642-38088-4_1
87 rdf:type schema:PropertyValue
88 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
89 schema:name Information and Computing Sciences
90 rdf:type schema:DefinedTerm
91 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
92 schema:name Computation Theory and Mathematics
93 rdf:type schema:DefinedTerm
94 sg:person.011367557177.46 schema:affiliation grid-institutes:grid.10267.32
95 schema:familyName Barnat
96 schema:givenName Jiří
97 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011367557177.46
98 rdf:type schema:Person
99 sg:person.0645117057.83 schema:affiliation grid-institutes:grid.10267.32
100 schema:familyName Brim
101 schema:givenName Luboš
102 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0645117057.83
103 rdf:type schema:Person
104 sg:person.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
105 schema:familyName Ročkai
106 schema:givenName Petr
107 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
108 rdf:type schema:Person
109 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
110 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
111 rdf:type schema:Organization
 




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


...