A Simulator for LLVM Bitcode View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2019-07-25

AUTHORS

Petr Ročkai , Jiří Barnat

ABSTRACT

In this paper, we introduce an interactive simulator for programs in the form of LLVM bitcode. The main features of the simulator include precise control over thread scheduling, automatic checkpoints and reverse stepping, support for source-level information about functions and variables in C and C++ programs and structured heap visualisation. Additionally, the simulator is compatible with DiVM (DIVINE VM) hypercalls, which makes it possible to load, simulate and analyse counterexamples from an existing model checker. More... »

PAGES

127-142

Book

TITLE

Formal Methods for Industrial Critical Systems

ISBN

978-3-030-27007-0
978-3-030-27008-7

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-030-27008-7_8

DOI

http://dx.doi.org/10.1007/978-3-030-27008-7_8

DIMENSIONS

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


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/0801", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Artificial Intelligence and Image Processing", 
        "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"
      }
    ], 
    "datePublished": "2019-07-25", 
    "datePublishedReg": "2019-07-25", 
    "description": "In this paper, we introduce an interactive simulator for programs in the form of LLVM bitcode. The main features of the simulator include precise control over thread scheduling, automatic checkpoints and reverse stepping, support for source-level information about functions and variables in C and C++ programs and structured heap visualisation. Additionally, the simulator is compatible with DiVM (DIVINE VM) hypercalls, which makes it possible to load, simulate and analyse counterexamples from an existing model checker.", 
    "editor": [
      {
        "familyName": "Larsen", 
        "givenName": "Kim Guldstrand", 
        "type": "Person"
      }, 
      {
        "familyName": "Willemse", 
        "givenName": "Tim", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-030-27008-7_8", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-030-27007-0", 
        "978-3-030-27008-7"
      ], 
      "name": "Formal Methods for Industrial Critical Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "LLVM bitcode", 
      "source-level information", 
      "interactive simulator", 
      "model checker", 
      "thread scheduling", 
      "simulator", 
      "hypercalls", 
      "checker", 
      "main features", 
      "scheduling", 
      "visualisation", 
      "information", 
      "features", 
      "program", 
      "counterexamples", 
      "support", 
      "stepping", 
      "precise control", 
      "checkpoint", 
      "control", 
      "function", 
      "form", 
      "variables", 
      "paper"
    ], 
    "name": "A Simulator for LLVM Bitcode", 
    "pagination": "127-142", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1120495016"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-030-27008-7_8"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-030-27008-7_8", 
      "https://app.dimensions.ai/details/publication/pub.1120495016"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-08-04T17:22", 
    "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_64.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-030-27008-7_8"
  }
]
 

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-030-27008-7_8'

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-030-27008-7_8'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-27008-7_8'

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-030-27008-7_8'


 

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

95 TRIPLES      22 PREDICATES      48 URIs      41 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-030-27008-7_8 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 schema:author N040d513fa4a647a2a8ba3eed41571e63
4 schema:datePublished 2019-07-25
5 schema:datePublishedReg 2019-07-25
6 schema:description In this paper, we introduce an interactive simulator for programs in the form of LLVM bitcode. The main features of the simulator include precise control over thread scheduling, automatic checkpoints and reverse stepping, support for source-level information about functions and variables in C and C++ programs and structured heap visualisation. Additionally, the simulator is compatible with DiVM (DIVINE VM) hypercalls, which makes it possible to load, simulate and analyse counterexamples from an existing model checker.
7 schema:editor Nc8f57a8d8e1d4f259464b6786611d864
8 schema:genre chapter
9 schema:isAccessibleForFree false
10 schema:isPartOf N0046c61007d54be6b1da07ac911b04fb
11 schema:keywords LLVM bitcode
12 checker
13 checkpoint
14 control
15 counterexamples
16 features
17 form
18 function
19 hypercalls
20 information
21 interactive simulator
22 main features
23 model checker
24 paper
25 precise control
26 program
27 scheduling
28 simulator
29 source-level information
30 stepping
31 support
32 thread scheduling
33 variables
34 visualisation
35 schema:name A Simulator for LLVM Bitcode
36 schema:pagination 127-142
37 schema:productId Neec317d1835046afa5a27327b3e2d6b3
38 Nfc386ecb55414177b6563bf0e3af00ed
39 schema:publisher N575296f7e1b14e25b0069678cbb58891
40 schema:sameAs https://app.dimensions.ai/details/publication/pub.1120495016
41 https://doi.org/10.1007/978-3-030-27008-7_8
42 schema:sdDatePublished 2022-08-04T17:22
43 schema:sdLicense https://scigraph.springernature.com/explorer/license/
44 schema:sdPublisher Ndc88719f2d824a948b285843088acabf
45 schema:url https://doi.org/10.1007/978-3-030-27008-7_8
46 sgo:license sg:explorer/license/
47 sgo:sdDataset chapters
48 rdf:type schema:Chapter
49 N0046c61007d54be6b1da07ac911b04fb schema:isbn 978-3-030-27007-0
50 978-3-030-27008-7
51 schema:name Formal Methods for Industrial Critical Systems
52 rdf:type schema:Book
53 N040d513fa4a647a2a8ba3eed41571e63 rdf:first sg:person.07377571657.86
54 rdf:rest N7e843f664abd4078bf0bdb8283a3e908
55 N56186eaad4464fd9b8ce1748622972ec schema:familyName Willemse
56 schema:givenName Tim
57 rdf:type schema:Person
58 N575296f7e1b14e25b0069678cbb58891 schema:name Springer Nature
59 rdf:type schema:Organisation
60 N7e843f664abd4078bf0bdb8283a3e908 rdf:first sg:person.011367557177.46
61 rdf:rest rdf:nil
62 Nbbb120b2e0264d5786cd7f2d8d834e21 rdf:first N56186eaad4464fd9b8ce1748622972ec
63 rdf:rest rdf:nil
64 Nc8f57a8d8e1d4f259464b6786611d864 rdf:first Nd61f2ef365dc4664970642dcb50841c0
65 rdf:rest Nbbb120b2e0264d5786cd7f2d8d834e21
66 Nd61f2ef365dc4664970642dcb50841c0 schema:familyName Larsen
67 schema:givenName Kim Guldstrand
68 rdf:type schema:Person
69 Ndc88719f2d824a948b285843088acabf schema:name Springer Nature - SN SciGraph project
70 rdf:type schema:Organization
71 Neec317d1835046afa5a27327b3e2d6b3 schema:name doi
72 schema:value 10.1007/978-3-030-27008-7_8
73 rdf:type schema:PropertyValue
74 Nfc386ecb55414177b6563bf0e3af00ed schema:name dimensions_id
75 schema:value pub.1120495016
76 rdf:type schema:PropertyValue
77 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
78 schema:name Information and Computing Sciences
79 rdf:type schema:DefinedTerm
80 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
81 schema:name Artificial Intelligence and Image Processing
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.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
89 schema:familyName Ročkai
90 schema:givenName Petr
91 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
92 rdf:type schema:Person
93 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
94 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
95 rdf:type schema:Organization
 




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


...