DivSIM , an interactive simulator for LLVM bitcode View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

2022-04-01

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, DivSIM is compatible with DiVM (DIVINE VM) hypercalls, which makes it possible to load, simulate and analyse counterexamples from an existing model checker, and with abstract bitcode generated by LART (LLVM Abstraction and Refinement Tool), making it suitable for direct analysis of abstract and/or symbolic programs and counterexamples. More... »

PAGES

493-510

References to SciGraph publications

  • 2019-04-04. Extending DIVINE with Symbolic Verification Using SMT in TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS
  • 2020-04-17. Symbiotic 7: Integration of Predator and More in TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS
  • 2012. Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs in FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS
  • 2013. Pro Objective-C in NONE
  • 2019-07-25. A Simulator for LLVM Bitcode in FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS
  • 2004. A Tutorial on Uppaal in FORMAL METHODS FOR THE DESIGN OF REAL-TIME SYSTEMS
  • 2003-04-15. What Went Wrong: Explaining Counterexamples in MODEL CHECKING SOFTWARE
  • 2004. SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft in INTEGRATED FORMAL METHODS
  • 2020-10-23. Reproducible execution of POSIX programs with DiOS in SOFTWARE AND SYSTEMS MODELING
  • 2016-04-09. Vienna Verification Tool: IC3 for Parallel Software in TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS
  • 2004. Understanding Counterexamples with explain in COMPUTER AIDED VERIFICATION
  • 2018-07-12. Statistical Model Checking of LLVM Code in FORMAL METHODS
  • 2016-07-07. Stateless model checking for TSO and PSO in ACTA INFORMATICA
  • 2018-10-15. Symbolic Computation via Program Transformation in THEORETICAL ASPECTS OF COMPUTING – ICTAC 2018
  • Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/s10009-022-00659-x

    DOI

    http://dx.doi.org/10.1007/s10009-022-00659-x

    DIMENSIONS

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


    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"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/978-3-030-27008-7_8", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1120495016", 
              "https://doi.org/10.1007/978-3-030-27008-7_8"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-24756-2_1", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1008623239", 
              "https://doi.org/10.1007/978-3-540-24756-2_1"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-30080-9_7", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1012450630", 
              "https://doi.org/10.1007/978-3-540-30080-9_7"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-1-4302-5051-7", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1024601409", 
              "https://doi.org/10.1007/978-1-4302-5051-7"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-27813-9_35", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1012132588", 
              "https://doi.org/10.1007/978-3-540-27813-9_35"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-32469-7_6", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1024950309", 
              "https://doi.org/10.1007/978-3-642-32469-7_6"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s00236-016-0275-0", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1000363069", 
              "https://doi.org/10.1007/s00236-016-0275-0"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-319-95582-7_32", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1105471602", 
              "https://doi.org/10.1007/978-3-319-95582-7_32"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-030-17502-3_14", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1113233409", 
              "https://doi.org/10.1007/978-3-030-17502-3_14"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-44829-2_8", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1001400839", 
              "https://doi.org/10.1007/3-540-44829-2_8"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-662-49674-9_69", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1007380353", 
              "https://doi.org/10.1007/978-3-662-49674-9_69"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-030-45237-7_31", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1126750739", 
              "https://doi.org/10.1007/978-3-030-45237-7_31"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/s10270-020-00837-y", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1132019834", 
              "https://doi.org/10.1007/s10270-020-00837-y"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-030-02508-3_17", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1107608889", 
              "https://doi.org/10.1007/978-3-030-02508-3_17"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2022-04-01", 
        "datePublishedReg": "2022-04-01", 
        "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, DivSIM is compatible with DiVM (DIVINE VM) hypercalls, which makes it possible to load, simulate and analyse counterexamples from an existing model checker, and with abstract bitcode generated by LART (LLVM Abstraction and Refinement Tool), making it suitable for direct analysis of abstract and/or symbolic programs and counterexamples.", 
        "genre": "article", 
        "id": "sg:pub.10.1007/s10009-022-00659-x", 
        "isAccessibleForFree": false, 
        "isPartOf": [
          {
            "id": "sg:journal.1052641", 
            "issn": [
              "1433-2779", 
              "1433-2787"
            ], 
            "name": "International Journal on Software Tools for Technology Transfer", 
            "publisher": "Springer Nature", 
            "type": "Periodical"
          }, 
          {
            "issueNumber": "3", 
            "type": "PublicationIssue"
          }, 
          {
            "type": "PublicationVolume", 
            "volumeNumber": "24"
          }
        ], 
        "keywords": [
          "interactive simulator", 
          "LLVM bitcode", 
          "source-level information", 
          "model checker", 
          "thread scheduling", 
          "symbolic program", 
          "simulator", 
          "hypercalls", 
          "checker", 
          "main features", 
          "scheduling", 
          "visualisation", 
          "LART", 
          "information", 
          "counterexamples", 
          "features", 
          "program", 
          "support", 
          "stepping", 
          "precise control", 
          "checkpoint", 
          "control", 
          "function", 
          "analysis", 
          "form", 
          "variables", 
          "direct analysis", 
          "paper"
        ], 
        "name": "DivSIM , an interactive simulator for LLVM bitcode", 
        "pagination": "493-510", 
        "productId": [
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1146807209"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/s10009-022-00659-x"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1007/s10009-022-00659-x", 
          "https://app.dimensions.ai/details/publication/pub.1146807209"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2022-08-04T17:12", 
        "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/article/article_924.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "https://doi.org/10.1007/s10009-022-00659-x"
      }
    ]
     

    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/s10009-022-00659-x'

    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/s10009-022-00659-x'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s10009-022-00659-x'

    RDF/XML is a standard XML format for linked data.

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/s10009-022-00659-x'


     

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

    148 TRIPLES      21 PREDICATES      66 URIs      44 LITERALS      6 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/s10009-022-00659-x schema:about anzsrc-for:08
    2 anzsrc-for:0801
    3 schema:author Nbfed094493844eb1b3219c4b1e163dc5
    4 schema:citation sg:pub.10.1007/3-540-44829-2_8
    5 sg:pub.10.1007/978-1-4302-5051-7
    6 sg:pub.10.1007/978-3-030-02508-3_17
    7 sg:pub.10.1007/978-3-030-17502-3_14
    8 sg:pub.10.1007/978-3-030-27008-7_8
    9 sg:pub.10.1007/978-3-030-45237-7_31
    10 sg:pub.10.1007/978-3-319-95582-7_32
    11 sg:pub.10.1007/978-3-540-24756-2_1
    12 sg:pub.10.1007/978-3-540-27813-9_35
    13 sg:pub.10.1007/978-3-540-30080-9_7
    14 sg:pub.10.1007/978-3-642-32469-7_6
    15 sg:pub.10.1007/978-3-662-49674-9_69
    16 sg:pub.10.1007/s00236-016-0275-0
    17 sg:pub.10.1007/s10270-020-00837-y
    18 schema:datePublished 2022-04-01
    19 schema:datePublishedReg 2022-04-01
    20 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, DivSIM is compatible with DiVM (DIVINE VM) hypercalls, which makes it possible to load, simulate and analyse counterexamples from an existing model checker, and with abstract bitcode generated by LART (LLVM Abstraction and Refinement Tool), making it suitable for direct analysis of abstract and/or symbolic programs and counterexamples.
    21 schema:genre article
    22 schema:isAccessibleForFree false
    23 schema:isPartOf N5d185a21612f4c5e85586aee6c2605d9
    24 N78f4627c61a44c108ceec01df7c9d05a
    25 sg:journal.1052641
    26 schema:keywords LART
    27 LLVM bitcode
    28 analysis
    29 checker
    30 checkpoint
    31 control
    32 counterexamples
    33 direct analysis
    34 features
    35 form
    36 function
    37 hypercalls
    38 information
    39 interactive simulator
    40 main features
    41 model checker
    42 paper
    43 precise control
    44 program
    45 scheduling
    46 simulator
    47 source-level information
    48 stepping
    49 support
    50 symbolic program
    51 thread scheduling
    52 variables
    53 visualisation
    54 schema:name DivSIM , an interactive simulator for LLVM bitcode
    55 schema:pagination 493-510
    56 schema:productId N705f673f7bfa49d3849d3c3164e19ecb
    57 N9bc32942f2594bf7bf68eeaceb264905
    58 schema:sameAs https://app.dimensions.ai/details/publication/pub.1146807209
    59 https://doi.org/10.1007/s10009-022-00659-x
    60 schema:sdDatePublished 2022-08-04T17:12
    61 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    62 schema:sdPublisher N141b7e1bf4d04c9eb33802b7e5351df2
    63 schema:url https://doi.org/10.1007/s10009-022-00659-x
    64 sgo:license sg:explorer/license/
    65 sgo:sdDataset articles
    66 rdf:type schema:ScholarlyArticle
    67 N141b7e1bf4d04c9eb33802b7e5351df2 schema:name Springer Nature - SN SciGraph project
    68 rdf:type schema:Organization
    69 N5d185a21612f4c5e85586aee6c2605d9 schema:issueNumber 3
    70 rdf:type schema:PublicationIssue
    71 N705f673f7bfa49d3849d3c3164e19ecb schema:name doi
    72 schema:value 10.1007/s10009-022-00659-x
    73 rdf:type schema:PropertyValue
    74 N78f4627c61a44c108ceec01df7c9d05a schema:volumeNumber 24
    75 rdf:type schema:PublicationVolume
    76 N9733ce1d2dc64699934580545e413dfc rdf:first sg:person.011367557177.46
    77 rdf:rest rdf:nil
    78 N9bc32942f2594bf7bf68eeaceb264905 schema:name dimensions_id
    79 schema:value pub.1146807209
    80 rdf:type schema:PropertyValue
    81 Nbfed094493844eb1b3219c4b1e163dc5 rdf:first sg:person.07377571657.86
    82 rdf:rest N9733ce1d2dc64699934580545e413dfc
    83 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    84 schema:name Information and Computing Sciences
    85 rdf:type schema:DefinedTerm
    86 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
    87 schema:name Artificial Intelligence and Image Processing
    88 rdf:type schema:DefinedTerm
    89 sg:journal.1052641 schema:issn 1433-2779
    90 1433-2787
    91 schema:name International Journal on Software Tools for Technology Transfer
    92 schema:publisher Springer Nature
    93 rdf:type schema:Periodical
    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.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
    100 schema:familyName Ročkai
    101 schema:givenName Petr
    102 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
    103 rdf:type schema:Person
    104 sg:pub.10.1007/3-540-44829-2_8 schema:sameAs https://app.dimensions.ai/details/publication/pub.1001400839
    105 https://doi.org/10.1007/3-540-44829-2_8
    106 rdf:type schema:CreativeWork
    107 sg:pub.10.1007/978-1-4302-5051-7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1024601409
    108 https://doi.org/10.1007/978-1-4302-5051-7
    109 rdf:type schema:CreativeWork
    110 sg:pub.10.1007/978-3-030-02508-3_17 schema:sameAs https://app.dimensions.ai/details/publication/pub.1107608889
    111 https://doi.org/10.1007/978-3-030-02508-3_17
    112 rdf:type schema:CreativeWork
    113 sg:pub.10.1007/978-3-030-17502-3_14 schema:sameAs https://app.dimensions.ai/details/publication/pub.1113233409
    114 https://doi.org/10.1007/978-3-030-17502-3_14
    115 rdf:type schema:CreativeWork
    116 sg:pub.10.1007/978-3-030-27008-7_8 schema:sameAs https://app.dimensions.ai/details/publication/pub.1120495016
    117 https://doi.org/10.1007/978-3-030-27008-7_8
    118 rdf:type schema:CreativeWork
    119 sg:pub.10.1007/978-3-030-45237-7_31 schema:sameAs https://app.dimensions.ai/details/publication/pub.1126750739
    120 https://doi.org/10.1007/978-3-030-45237-7_31
    121 rdf:type schema:CreativeWork
    122 sg:pub.10.1007/978-3-319-95582-7_32 schema:sameAs https://app.dimensions.ai/details/publication/pub.1105471602
    123 https://doi.org/10.1007/978-3-319-95582-7_32
    124 rdf:type schema:CreativeWork
    125 sg:pub.10.1007/978-3-540-24756-2_1 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008623239
    126 https://doi.org/10.1007/978-3-540-24756-2_1
    127 rdf:type schema:CreativeWork
    128 sg:pub.10.1007/978-3-540-27813-9_35 schema:sameAs https://app.dimensions.ai/details/publication/pub.1012132588
    129 https://doi.org/10.1007/978-3-540-27813-9_35
    130 rdf:type schema:CreativeWork
    131 sg:pub.10.1007/978-3-540-30080-9_7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1012450630
    132 https://doi.org/10.1007/978-3-540-30080-9_7
    133 rdf:type schema:CreativeWork
    134 sg:pub.10.1007/978-3-642-32469-7_6 schema:sameAs https://app.dimensions.ai/details/publication/pub.1024950309
    135 https://doi.org/10.1007/978-3-642-32469-7_6
    136 rdf:type schema:CreativeWork
    137 sg:pub.10.1007/978-3-662-49674-9_69 schema:sameAs https://app.dimensions.ai/details/publication/pub.1007380353
    138 https://doi.org/10.1007/978-3-662-49674-9_69
    139 rdf:type schema:CreativeWork
    140 sg:pub.10.1007/s00236-016-0275-0 schema:sameAs https://app.dimensions.ai/details/publication/pub.1000363069
    141 https://doi.org/10.1007/s00236-016-0275-0
    142 rdf:type schema:CreativeWork
    143 sg:pub.10.1007/s10270-020-00837-y schema:sameAs https://app.dimensions.ai/details/publication/pub.1132019834
    144 https://doi.org/10.1007/s10270-020-00837-y
    145 rdf:type schema:CreativeWork
    146 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
    147 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
    148 rdf:type schema:Organization
     




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


    ...