Ontology type: schema:Chapter Open Access: True
2019-04-04
AUTHORSHenrich Lauko , Vladimír Štill , Petr Ročkai , Jiří Barnat
ABSTRACTDIVINE is an LLVM-based verification tool focusing on analysis of real-world C and C++ programs. Such programs often interact with their environment, for example via inputs from users or network. When these programs are analyzed, it is desirable that the verification tool can deal with inputs symbolically and analyze runs for all inputs. In DIVINE, it is now possible to deal with input data via symbolic computation instrumented into the original program at the level of LLVM bitcode. Such an instrumented program maintains symbolic values internally and operates directly on them. Instrumentation allows us to enhance the tool with support for symbolic data without substantial modifications of the tool itself. Namely, this competition contribution uses SMT formulae for representation of input data. More... »
PAGES204-208
Tools and Algorithms for the Construction and Analysis of Systems
ISBN
978-3-030-17501-6
978-3-030-17502-3
http://scigraph.springernature.com/pub.10.1007/978-3-030-17502-3_14
DOIhttp://dx.doi.org/10.1007/978-3-030-17502-3_14
DIMENSIONShttps://app.dimensions.ai/details/publication/pub.1113233409
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/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": "\u0160till",
"givenName": "Vladim\u00edr",
"id": "sg:person.016057731543.01",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016057731543.01"
],
"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"
},
{
"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-04-04",
"datePublishedReg": "2019-04-04",
"description": "DIVINE is an LLVM-based verification tool focusing on analysis of real-world C and C++ programs. Such programs often interact with their environment, for example via inputs from users or network. When these programs are analyzed, it is desirable that the verification tool can deal with inputs symbolically and analyze runs for all inputs. In DIVINE, it is now possible to deal with input data via symbolic computation instrumented into the original program at the level of LLVM bitcode. Such an instrumented program maintains symbolic values internally and operates directly on them. Instrumentation allows us to enhance the tool with support for symbolic data without substantial modifications of the tool itself. Namely, this competition contribution uses SMT formulae for representation of input data.",
"editor": [
{
"familyName": "Beyer",
"givenName": "Dirk",
"type": "Person"
},
{
"familyName": "Huisman",
"givenName": "Marieke",
"type": "Person"
},
{
"familyName": "Kordon",
"givenName": "Fabrice",
"type": "Person"
},
{
"familyName": "Steffen",
"givenName": "Bernhard",
"type": "Person"
}
],
"genre": "chapter",
"id": "sg:pub.10.1007/978-3-030-17502-3_14",
"isAccessibleForFree": true,
"isPartOf": {
"isbn": [
"978-3-030-17501-6",
"978-3-030-17502-3"
],
"name": "Tools and Algorithms for the Construction and Analysis of Systems",
"type": "Book"
},
"keywords": [
"verification tools",
"input data",
"symbolic verification",
"symbolic data",
"instrumented program",
"SMT formulas",
"LLVM bitcode",
"original program",
"symbolic computation",
"LLVM",
"tool",
"users",
"input",
"network",
"computation",
"verification",
"SMT",
"representation",
"data",
"environment",
"program",
"such programs",
"example",
"support",
"symbolic value",
"run",
"instrumentation",
"contribution",
"substantial modification",
"analysis",
"modification",
"formula",
"values",
"levels",
"divine"
],
"name": "Extending DIVINE with Symbolic Verification Using SMT",
"pagination": "204-208",
"productId": [
{
"name": "dimensions_id",
"type": "PropertyValue",
"value": [
"pub.1113233409"
]
},
{
"name": "doi",
"type": "PropertyValue",
"value": [
"10.1007/978-3-030-17502-3_14"
]
}
],
"publisher": {
"name": "Springer Nature",
"type": "Organisation"
},
"sameAs": [
"https://doi.org/10.1007/978-3-030-17502-3_14",
"https://app.dimensions.ai/details/publication/pub.1113233409"
],
"sdDataset": "chapters",
"sdDatePublished": "2022-08-04T17:13",
"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_102.jsonl",
"type": "Chapter",
"url": "https://doi.org/10.1007/978-3-030-17502-3_14"
}
]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-17502-3_14'
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-17502-3_14'
Turtle is a human-readable linked data format.
curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-030-17502-3_14'
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-17502-3_14'
This table displays all metadata directly associated to this object as RDF triples.
130 TRIPLES
22 PREDICATES
59 URIs
52 LITERALS
7 BLANK NODES