LART: Compiled Abstract Execution View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2022-03-30

AUTHORS

Henrich Lauko , Petr Ročkai

ABSTRACT

lart – llvm abstraction and refinement tool – originates from the divine model-checker [5, 7], in which it was employed as an abstraction toolchain for the llvm interpreter. In this contribution, we present a stand-alone tool that does not need a verification backend but performs the verification natively. The core idea is to instrument abstract semantics directly into the program and compile it into a native binary that performs program analysis. This approach provides a performance gain of native execution over the interpreted analysis and allows compiler optimizations to be employed on abstracted code, further extending the analysis efficiency. Compilation-based abstraction introduces new challenges solved by lart, like domain interaction of concrete and abstract values simulation of nondeterministic runtime or constraint propagation. More... »

PAGES

457-461

Book

TITLE

Tools and Algorithms for the Construction and Analysis of Systems

ISBN

978-3-030-99526-3
978-3-030-99527-0

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-030-99527-0_31

DOI

http://dx.doi.org/10.1007/978-3-030-99527-0_31

DIMENSIONS

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


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"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0803", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computer Software", 
        "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": "Lauko", 
        "givenName": "Henrich", 
        "id": "sg:person.010156102043.29", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010156102043.29"
        ], 
        "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"
      }
    ], 
    "datePublished": "2022-03-30", 
    "datePublishedReg": "2022-03-30", 
    "description": "Abstractlart \u2013 llvm abstraction and refinement tool \u2013 originates from the divine model-checker [5, 7], in which it was employed as an abstraction toolchain for the llvm interpreter. In this contribution, we present a stand-alone tool that does not need a verification backend but performs the verification natively. The core idea is to instrument abstract semantics directly into the program and compile it into a native binary that performs program analysis. This approach provides a performance gain of native execution over the interpreted analysis and allows compiler optimizations to be employed on abstracted code, further extending the analysis efficiency. Compilation-based abstraction introduces new challenges solved by lart, like domain interaction of concrete and abstract values simulation of nondeterministic runtime or constraint propagation.", 
    "editor": [
      {
        "familyName": "Fisman", 
        "givenName": "Dana", 
        "type": "Person"
      }, 
      {
        "familyName": "Rosu", 
        "givenName": "Grigore", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-030-99527-0_31", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-030-99526-3", 
        "978-3-030-99527-0"
      ], 
      "name": "Tools and Algorithms for the Construction and Analysis of Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "stand-alone tool", 
      "native execution", 
      "abstract execution", 
      "verification backend", 
      "compiler optimizations", 
      "native binaries", 
      "program analysis", 
      "constraint propagation", 
      "abstract semantics", 
      "performance gains", 
      "core idea", 
      "analysis efficiency", 
      "new challenges", 
      "execution", 
      "abstraction", 
      "toolchain", 
      "backend", 
      "runtime", 
      "semantics", 
      "value simulation", 
      "verification", 
      "code", 
      "LART", 
      "interpreters", 
      "optimization", 
      "tool", 
      "challenges", 
      "idea", 
      "simulations", 
      "efficiency", 
      "refinement", 
      "binaries", 
      "program", 
      "analysis", 
      "gain", 
      "contribution", 
      "propagation", 
      "interaction", 
      "domain interactions", 
      "approach"
    ], 
    "name": "LART: Compiled Abstract Execution", 
    "pagination": "457-461", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1146682830"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-030-99527-0_31"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-030-99527-0_31", 
      "https://app.dimensions.ai/details/publication/pub.1146682830"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-08-04T17:18", 
    "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_342.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-030-99527-0_31"
  }
]
 

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-99527-0_31'

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-99527-0_31'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-99527-0_31'

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-99527-0_31'


 

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

115 TRIPLES      22 PREDICATES      65 URIs      57 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-030-99527-0_31 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 anzsrc-for:0803
4 schema:author N82623949991945c7bd3856c578b0b592
5 schema:datePublished 2022-03-30
6 schema:datePublishedReg 2022-03-30
7 schema:description Abstractlart – llvm abstraction and refinement tool – originates from the divine model-checker [5, 7], in which it was employed as an abstraction toolchain for the llvm interpreter. In this contribution, we present a stand-alone tool that does not need a verification backend but performs the verification natively. The core idea is to instrument abstract semantics directly into the program and compile it into a native binary that performs program analysis. This approach provides a performance gain of native execution over the interpreted analysis and allows compiler optimizations to be employed on abstracted code, further extending the analysis efficiency. Compilation-based abstraction introduces new challenges solved by lart, like domain interaction of concrete and abstract values simulation of nondeterministic runtime or constraint propagation.
8 schema:editor Ncb71ff5bf2ae4bc2bd205680a1ef8747
9 schema:genre chapter
10 schema:isAccessibleForFree true
11 schema:isPartOf Nd1db59c4e9fd4128a356919ac3cede15
12 schema:keywords LART
13 abstract execution
14 abstract semantics
15 abstraction
16 analysis
17 analysis efficiency
18 approach
19 backend
20 binaries
21 challenges
22 code
23 compiler optimizations
24 constraint propagation
25 contribution
26 core idea
27 domain interactions
28 efficiency
29 execution
30 gain
31 idea
32 interaction
33 interpreters
34 native binaries
35 native execution
36 new challenges
37 optimization
38 performance gains
39 program
40 program analysis
41 propagation
42 refinement
43 runtime
44 semantics
45 simulations
46 stand-alone tool
47 tool
48 toolchain
49 value simulation
50 verification
51 verification backend
52 schema:name LART: Compiled Abstract Execution
53 schema:pagination 457-461
54 schema:productId Nd5ccde6f7fe946bf9484fd5efd4799ad
55 Neaa3cc97b3ed43099e8a248433331efd
56 schema:publisher N8c0196358037478bb5c32dce27e8a9bc
57 schema:sameAs https://app.dimensions.ai/details/publication/pub.1146682830
58 https://doi.org/10.1007/978-3-030-99527-0_31
59 schema:sdDatePublished 2022-08-04T17:18
60 schema:sdLicense https://scigraph.springernature.com/explorer/license/
61 schema:sdPublisher N5e38aa3a38ee4197bea7f54b4f2b454e
62 schema:url https://doi.org/10.1007/978-3-030-99527-0_31
63 sgo:license sg:explorer/license/
64 sgo:sdDataset chapters
65 rdf:type schema:Chapter
66 N0b18c76b63e44c91805feaf1d9142c04 schema:familyName Fisman
67 schema:givenName Dana
68 rdf:type schema:Person
69 N0b592b320111436ead7fa5ffd6fa78e4 rdf:first sg:person.07377571657.86
70 rdf:rest rdf:nil
71 N355890916bdf41c89109377d300a6abe schema:familyName Rosu
72 schema:givenName Grigore
73 rdf:type schema:Person
74 N5e38aa3a38ee4197bea7f54b4f2b454e schema:name Springer Nature - SN SciGraph project
75 rdf:type schema:Organization
76 N82623949991945c7bd3856c578b0b592 rdf:first sg:person.010156102043.29
77 rdf:rest N0b592b320111436ead7fa5ffd6fa78e4
78 N8c0196358037478bb5c32dce27e8a9bc schema:name Springer Nature
79 rdf:type schema:Organisation
80 Na702ca47adfd4ecbbb989605acb11b0d rdf:first N355890916bdf41c89109377d300a6abe
81 rdf:rest rdf:nil
82 Ncb71ff5bf2ae4bc2bd205680a1ef8747 rdf:first N0b18c76b63e44c91805feaf1d9142c04
83 rdf:rest Na702ca47adfd4ecbbb989605acb11b0d
84 Nd1db59c4e9fd4128a356919ac3cede15 schema:isbn 978-3-030-99526-3
85 978-3-030-99527-0
86 schema:name Tools and Algorithms for the Construction and Analysis of Systems
87 rdf:type schema:Book
88 Nd5ccde6f7fe946bf9484fd5efd4799ad schema:name dimensions_id
89 schema:value pub.1146682830
90 rdf:type schema:PropertyValue
91 Neaa3cc97b3ed43099e8a248433331efd schema:name doi
92 schema:value 10.1007/978-3-030-99527-0_31
93 rdf:type schema:PropertyValue
94 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
95 schema:name Information and Computing Sciences
96 rdf:type schema:DefinedTerm
97 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
98 schema:name Computation Theory and Mathematics
99 rdf:type schema:DefinedTerm
100 anzsrc-for:0803 schema:inDefinedTermSet anzsrc-for:
101 schema:name Computer Software
102 rdf:type schema:DefinedTerm
103 sg:person.010156102043.29 schema:affiliation grid-institutes:grid.10267.32
104 schema:familyName Lauko
105 schema:givenName Henrich
106 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010156102043.29
107 rdf:type schema:Person
108 sg:person.07377571657.86 schema:affiliation grid-institutes:grid.10267.32
109 schema:familyName Ročkai
110 schema:givenName Petr
111 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07377571657.86
112 rdf:type schema:Person
113 grid-institutes:grid.10267.32 schema:alternateName Faculty of Informatics, Masaryk University, Brno, Czech Republic
114 schema:name Faculty of Informatics, Masaryk University, Brno, Czech Republic
115 rdf:type schema:Organization
 




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


...