2022-03-30
AUTHORS 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. More... »
PAGES457-461
Tools and Algorithms for the Construction and Analysis of Systems
ISBN
978-3-030-99526-3
978-3-030-99527-0
http://scigraph.springernature.com/pub.10.1007/978-3-030-99527-0_31
DOIhttp://dx.doi.org/10.1007/978-3-030-99527-0_31
DIMENSIONShttps://app.dimensions.ai/details/publication/pub.1146682830
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
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 |