Separation Logic with One Quantified Variable View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

2017-08

AUTHORS

Stéphane Demri, Didier Galmiche, Dominique Larchey-Wendling, Daniel Méry

ABSTRACT

We investigate first-order separation logic with one record field restricted to a unique quantified variable (1SL1). Undecidability is known when the number of quantified variables is unbounded and the satisfiability problem is PSPACE-complete for the propositional fragment. We show that the satisfiability problem for 1SL1 is PSPACE-complete and we characterize its expressive power by showing that every formula is equivalent to a Boolean combination of atomic properties. This contributes to our understanding of fragments of first-order separation logic that can specify properties about the memory heap of programs with singly-linked lists. All the fragments we consider contain the magic wand operator and first-order quantification over a single variable. More... »

PAGES

371-461

References to SciGraph publications

  • 2013. Automating Separation Logic Using SMT in COMPUTER AIDED VERIFICATION
  • 2013. SeLoger: A Tool for Graph-Based Reasoning in Separation Logic in COMPUTER AIDED VERIFICATION
  • 2006. Smallfoot: Modular Automatic Assertion Checking with Separation Logic in FORMAL METHODS FOR COMPONENTS AND OBJECTS
  • 2014. Foundations for Decision Problems in Separation Logic with General Inductive Predicates in FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES
  • 2011. CVC4 in COMPUTER AIDED VERIFICATION
  • 2013. Separation Logic Modulo Theories in PROGRAMMING LANGUAGES AND SYSTEMS
  • 2008. Z3: An Efficient SMT Solver in TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS
  • 2001. Computability and Complexity Results for a Spatial Assertion Language for Data Structures in FST TCS 2001: FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE
  • 2011. Tractable Reasoning in a Fragment of Separation Logic in CONCUR 2011 – CONCURRENCY THEORY
  • 2014. Separation Logic with One Quantified Variable in COMPUTER SCIENCE - THEORY AND APPLICATIONS
  • 2013. The Tree Width of Separation Logic with Recursive Definitions in AUTOMATED DEDUCTION – CADE-24
  • 2015. Deciding Local Theory Extensions via E-matching in COMPUTER AIDED VERIFICATION
  • 2014. GRASShopper in TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS
  • Identifiers

    URI

    http://scigraph.springernature.com/pub.10.1007/s00224-016-9713-1

    DOI

    http://dx.doi.org/10.1007/s00224-016-9713-1

    DIMENSIONS

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


    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/2203", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Philosophy", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/22", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Philosophy and Religious Studies", 
            "type": "DefinedTerm"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "Laboratoire Sp\u00e9cification et V\u00e9rification", 
              "id": "https://www.grid.ac/institutes/grid.464035.0", 
              "name": [
                "LSV, ENS Paris-Saclay, CNRS, Universit\u00e9 Paris-Saclay, Cachan, France"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Demri", 
            "givenName": "St\u00e9phane", 
            "id": "sg:person.016112550611.96", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016112550611.96"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Lorraine Research Laboratory in Computer Science and its Applications", 
              "id": "https://www.grid.ac/institutes/grid.462764.5", 
              "name": [
                "LORIA, Universit\u00e9 de Lorraine, BP 239, 54506, Vand\u0153uvre-l\u00e8s-Nancy, France"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Galmiche", 
            "givenName": "Didier", 
            "id": "sg:person.07677466522.93", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07677466522.93"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "French National Centre for Scientific Research", 
              "id": "https://www.grid.ac/institutes/grid.4444.0", 
              "name": [
                "LORIA, CNRS, BP 239, 54506, Vand\u0153uvre-l\u00e8s-Nancy, France"
              ], 
              "type": "Organization"
            }, 
            "familyName": "Larchey-Wendling", 
            "givenName": "Dominique", 
            "id": "sg:person.015171354765.75", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015171354765.75"
            ], 
            "type": "Person"
          }, 
          {
            "affiliation": {
              "alternateName": "Lorraine Research Laboratory in Computer Science and its Applications", 
              "id": "https://www.grid.ac/institutes/grid.462764.5", 
              "name": [
                "LORIA, Universit\u00e9 de Lorraine, BP 239, 54506, Vand\u0153uvre-l\u00e8s-Nancy, France"
              ], 
              "type": "Organization"
            }, 
            "familyName": "M\u00e9ry", 
            "givenName": "Daniel", 
            "id": "sg:person.010036446656.28", 
            "sameAs": [
              "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010036446656.28"
            ], 
            "type": "Person"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/978-3-642-22110-1_14", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1002288082", 
              "https://doi.org/10.1007/978-3-642-22110-1_14"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-22110-1_14", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1002288082", 
              "https://doi.org/10.1007/978-3-642-22110-1_14"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-54830-7_27", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1002317769", 
              "https://doi.org/10.1007/978-3-642-54830-7_27"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/2603088.2603142", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1004660694"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-319-21668-3_6", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1009223056", 
              "https://doi.org/10.1007/978-3-319-21668-3_6"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/j.ic.2006.10.006", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1013214343"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-54862-8_9", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1018478677", 
              "https://doi.org/10.1007/978-3-642-54862-8_9"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-23217-6_16", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1030741306", 
              "https://doi.org/10.1007/978-3-642-23217-6_16"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-23217-6_16", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1030741306", 
              "https://doi.org/10.1007/978-3-642-23217-6_16"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-319-03542-0_7", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1032299332", 
              "https://doi.org/10.1007/978-3-319-03542-0_7"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/2603088.2603091", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1033197618"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-78800-3_24", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1034005359", 
              "https://doi.org/10.1007/978-3-540-78800-3_24"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-540-78800-3_24", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1034005359", 
              "https://doi.org/10.1007/978-3-540-78800-3_24"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11804192_6", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1034592185", 
              "https://doi.org/10.1007/11804192_6"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/11804192_6", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1034592185", 
              "https://doi.org/10.1007/11804192_6"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/j.ic.2011.12.003", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1038142559"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-39799-8_54", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1041413530", 
              "https://doi.org/10.1007/978-3-642-39799-8_54"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1016/j.apal.2009.07.004", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1044429714"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-38574-2_2", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1044572416", 
              "https://doi.org/10.1007/978-3-642-38574-2_2"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-642-39799-8_55", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1045585361", 
              "https://doi.org/10.1007/978-3-642-39799-8_55"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/3-540-45294-x_10", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1053274511", 
              "https://doi.org/10.1007/3-540-45294-x_10"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "sg:pub.10.1007/978-3-319-06686-8_10", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1053523033", 
              "https://doi.org/10.1007/978-3-319-06686-8_10"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1093/logcom/exn066", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1059876216"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/lics.2010.24", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1095059117"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/lics.2010.18", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1095349123"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1109/lics.2002.1029817", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1095718758"
            ], 
            "type": "CreativeWork"
          }, 
          {
            "id": "https://doi.org/10.1145/360204.375719", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1098890971"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "2017-08", 
        "datePublishedReg": "2017-08-01", 
        "description": "We investigate first-order separation logic with one record field restricted to a unique quantified variable (1SL1). Undecidability is known when the number of quantified variables is unbounded and the satisfiability problem is PSPACE-complete for the propositional fragment. We show that the satisfiability problem for 1SL1 is PSPACE-complete and we characterize its expressive power by showing that every formula is equivalent to a Boolean combination of atomic properties. This contributes to our understanding of fragments of first-order separation logic that can specify properties about the memory heap of programs with singly-linked lists. All the fragments we consider contain the magic wand operator and first-order quantification over a single variable.", 
        "genre": "research_article", 
        "id": "sg:pub.10.1007/s00224-016-9713-1", 
        "inLanguage": [
          "en"
        ], 
        "isAccessibleForFree": false, 
        "isPartOf": [
          {
            "id": "sg:journal.1052098", 
            "issn": [
              "1432-4350", 
              "1433-0490"
            ], 
            "name": "Theory of Computing Systems", 
            "type": "Periodical"
          }, 
          {
            "issueNumber": "2", 
            "type": "PublicationIssue"
          }, 
          {
            "type": "PublicationVolume", 
            "volumeNumber": "61"
          }
        ], 
        "name": "Separation Logic with One Quantified Variable", 
        "pagination": "371-461", 
        "productId": [
          {
            "name": "readcube_id", 
            "type": "PropertyValue", 
            "value": [
              "51b5f0b21e6908e51742a5a168318b263b6dd6a49b6970197e27fdc493dfb6e8"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/s00224-016-9713-1"
            ]
          }, 
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1085719728"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1007/s00224-016-9713-1", 
          "https://app.dimensions.ai/details/publication/pub.1085719728"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2019-04-11T12:21", 
        "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
        "sdPublisher": {
          "name": "Springer Nature - SN SciGraph project", 
          "type": "Organization"
        }, 
        "sdSource": "s3://com-uberresearch-data-dimensions-target-20181106-alternative/cleanup/v134/2549eaecd7973599484d7c17b260dba0a4ecb94b/merge/v9/a6c9fde33151104705d4d7ff012ea9563521a3ce/jats-lookup/v90/0000000362_0000000362/records_87078_00000001.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "https://link.springer.com/10.1007%2Fs00224-016-9713-1"
      }
    ]
     

    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/s00224-016-9713-1'

    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/s00224-016-9713-1'

    Turtle is a human-readable linked data format.

    curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/s00224-016-9713-1'

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

    curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/s00224-016-9713-1'


     

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

    170 TRIPLES      21 PREDICATES      50 URIs      19 LITERALS      7 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/s00224-016-9713-1 schema:about anzsrc-for:22
    2 anzsrc-for:2203
    3 schema:author N837d8c12a76c441b84d85094e1b8e3fa
    4 schema:citation sg:pub.10.1007/11804192_6
    5 sg:pub.10.1007/3-540-45294-x_10
    6 sg:pub.10.1007/978-3-319-03542-0_7
    7 sg:pub.10.1007/978-3-319-06686-8_10
    8 sg:pub.10.1007/978-3-319-21668-3_6
    9 sg:pub.10.1007/978-3-540-78800-3_24
    10 sg:pub.10.1007/978-3-642-22110-1_14
    11 sg:pub.10.1007/978-3-642-23217-6_16
    12 sg:pub.10.1007/978-3-642-38574-2_2
    13 sg:pub.10.1007/978-3-642-39799-8_54
    14 sg:pub.10.1007/978-3-642-39799-8_55
    15 sg:pub.10.1007/978-3-642-54830-7_27
    16 sg:pub.10.1007/978-3-642-54862-8_9
    17 https://doi.org/10.1016/j.apal.2009.07.004
    18 https://doi.org/10.1016/j.ic.2006.10.006
    19 https://doi.org/10.1016/j.ic.2011.12.003
    20 https://doi.org/10.1093/logcom/exn066
    21 https://doi.org/10.1109/lics.2002.1029817
    22 https://doi.org/10.1109/lics.2010.18
    23 https://doi.org/10.1109/lics.2010.24
    24 https://doi.org/10.1145/2603088.2603091
    25 https://doi.org/10.1145/2603088.2603142
    26 https://doi.org/10.1145/360204.375719
    27 schema:datePublished 2017-08
    28 schema:datePublishedReg 2017-08-01
    29 schema:description We investigate first-order separation logic with one record field restricted to a unique quantified variable (1SL1). Undecidability is known when the number of quantified variables is unbounded and the satisfiability problem is PSPACE-complete for the propositional fragment. We show that the satisfiability problem for 1SL1 is PSPACE-complete and we characterize its expressive power by showing that every formula is equivalent to a Boolean combination of atomic properties. This contributes to our understanding of fragments of first-order separation logic that can specify properties about the memory heap of programs with singly-linked lists. All the fragments we consider contain the magic wand operator and first-order quantification over a single variable.
    30 schema:genre research_article
    31 schema:inLanguage en
    32 schema:isAccessibleForFree false
    33 schema:isPartOf N9572612d54da44319938b758bda15f9b
    34 Neefcf86e55ad4b6ea6669c2c9b095138
    35 sg:journal.1052098
    36 schema:name Separation Logic with One Quantified Variable
    37 schema:pagination 371-461
    38 schema:productId N34a4fdb935c44445a01f92add5fed338
    39 N4b93d4fc158c4498a42c0bd50a26d369
    40 Nc6e3bad0745048b984f4bcb61aefd661
    41 schema:sameAs https://app.dimensions.ai/details/publication/pub.1085719728
    42 https://doi.org/10.1007/s00224-016-9713-1
    43 schema:sdDatePublished 2019-04-11T12:21
    44 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    45 schema:sdPublisher Nc93cd53b83d140e3bdb84d35e11e529c
    46 schema:url https://link.springer.com/10.1007%2Fs00224-016-9713-1
    47 sgo:license sg:explorer/license/
    48 sgo:sdDataset articles
    49 rdf:type schema:ScholarlyArticle
    50 N2f5d72797a2947ed97ba4a5c7d61f614 rdf:first sg:person.07677466522.93
    51 rdf:rest Ndb6f8dcfc0e94c9fb57112ae9ef76204
    52 N34a4fdb935c44445a01f92add5fed338 schema:name dimensions_id
    53 schema:value pub.1085719728
    54 rdf:type schema:PropertyValue
    55 N4b93d4fc158c4498a42c0bd50a26d369 schema:name doi
    56 schema:value 10.1007/s00224-016-9713-1
    57 rdf:type schema:PropertyValue
    58 N837d8c12a76c441b84d85094e1b8e3fa rdf:first sg:person.016112550611.96
    59 rdf:rest N2f5d72797a2947ed97ba4a5c7d61f614
    60 N9572612d54da44319938b758bda15f9b schema:issueNumber 2
    61 rdf:type schema:PublicationIssue
    62 Nbd1677d343504fb38b57d69c32a9c8c6 rdf:first sg:person.010036446656.28
    63 rdf:rest rdf:nil
    64 Nc6e3bad0745048b984f4bcb61aefd661 schema:name readcube_id
    65 schema:value 51b5f0b21e6908e51742a5a168318b263b6dd6a49b6970197e27fdc493dfb6e8
    66 rdf:type schema:PropertyValue
    67 Nc93cd53b83d140e3bdb84d35e11e529c schema:name Springer Nature - SN SciGraph project
    68 rdf:type schema:Organization
    69 Ndb6f8dcfc0e94c9fb57112ae9ef76204 rdf:first sg:person.015171354765.75
    70 rdf:rest Nbd1677d343504fb38b57d69c32a9c8c6
    71 Neefcf86e55ad4b6ea6669c2c9b095138 schema:volumeNumber 61
    72 rdf:type schema:PublicationVolume
    73 anzsrc-for:22 schema:inDefinedTermSet anzsrc-for:
    74 schema:name Philosophy and Religious Studies
    75 rdf:type schema:DefinedTerm
    76 anzsrc-for:2203 schema:inDefinedTermSet anzsrc-for:
    77 schema:name Philosophy
    78 rdf:type schema:DefinedTerm
    79 sg:journal.1052098 schema:issn 1432-4350
    80 1433-0490
    81 schema:name Theory of Computing Systems
    82 rdf:type schema:Periodical
    83 sg:person.010036446656.28 schema:affiliation https://www.grid.ac/institutes/grid.462764.5
    84 schema:familyName Méry
    85 schema:givenName Daniel
    86 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010036446656.28
    87 rdf:type schema:Person
    88 sg:person.015171354765.75 schema:affiliation https://www.grid.ac/institutes/grid.4444.0
    89 schema:familyName Larchey-Wendling
    90 schema:givenName Dominique
    91 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015171354765.75
    92 rdf:type schema:Person
    93 sg:person.016112550611.96 schema:affiliation https://www.grid.ac/institutes/grid.464035.0
    94 schema:familyName Demri
    95 schema:givenName Stéphane
    96 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.016112550611.96
    97 rdf:type schema:Person
    98 sg:person.07677466522.93 schema:affiliation https://www.grid.ac/institutes/grid.462764.5
    99 schema:familyName Galmiche
    100 schema:givenName Didier
    101 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07677466522.93
    102 rdf:type schema:Person
    103 sg:pub.10.1007/11804192_6 schema:sameAs https://app.dimensions.ai/details/publication/pub.1034592185
    104 https://doi.org/10.1007/11804192_6
    105 rdf:type schema:CreativeWork
    106 sg:pub.10.1007/3-540-45294-x_10 schema:sameAs https://app.dimensions.ai/details/publication/pub.1053274511
    107 https://doi.org/10.1007/3-540-45294-x_10
    108 rdf:type schema:CreativeWork
    109 sg:pub.10.1007/978-3-319-03542-0_7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1032299332
    110 https://doi.org/10.1007/978-3-319-03542-0_7
    111 rdf:type schema:CreativeWork
    112 sg:pub.10.1007/978-3-319-06686-8_10 schema:sameAs https://app.dimensions.ai/details/publication/pub.1053523033
    113 https://doi.org/10.1007/978-3-319-06686-8_10
    114 rdf:type schema:CreativeWork
    115 sg:pub.10.1007/978-3-319-21668-3_6 schema:sameAs https://app.dimensions.ai/details/publication/pub.1009223056
    116 https://doi.org/10.1007/978-3-319-21668-3_6
    117 rdf:type schema:CreativeWork
    118 sg:pub.10.1007/978-3-540-78800-3_24 schema:sameAs https://app.dimensions.ai/details/publication/pub.1034005359
    119 https://doi.org/10.1007/978-3-540-78800-3_24
    120 rdf:type schema:CreativeWork
    121 sg:pub.10.1007/978-3-642-22110-1_14 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002288082
    122 https://doi.org/10.1007/978-3-642-22110-1_14
    123 rdf:type schema:CreativeWork
    124 sg:pub.10.1007/978-3-642-23217-6_16 schema:sameAs https://app.dimensions.ai/details/publication/pub.1030741306
    125 https://doi.org/10.1007/978-3-642-23217-6_16
    126 rdf:type schema:CreativeWork
    127 sg:pub.10.1007/978-3-642-38574-2_2 schema:sameAs https://app.dimensions.ai/details/publication/pub.1044572416
    128 https://doi.org/10.1007/978-3-642-38574-2_2
    129 rdf:type schema:CreativeWork
    130 sg:pub.10.1007/978-3-642-39799-8_54 schema:sameAs https://app.dimensions.ai/details/publication/pub.1041413530
    131 https://doi.org/10.1007/978-3-642-39799-8_54
    132 rdf:type schema:CreativeWork
    133 sg:pub.10.1007/978-3-642-39799-8_55 schema:sameAs https://app.dimensions.ai/details/publication/pub.1045585361
    134 https://doi.org/10.1007/978-3-642-39799-8_55
    135 rdf:type schema:CreativeWork
    136 sg:pub.10.1007/978-3-642-54830-7_27 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002317769
    137 https://doi.org/10.1007/978-3-642-54830-7_27
    138 rdf:type schema:CreativeWork
    139 sg:pub.10.1007/978-3-642-54862-8_9 schema:sameAs https://app.dimensions.ai/details/publication/pub.1018478677
    140 https://doi.org/10.1007/978-3-642-54862-8_9
    141 rdf:type schema:CreativeWork
    142 https://doi.org/10.1016/j.apal.2009.07.004 schema:sameAs https://app.dimensions.ai/details/publication/pub.1044429714
    143 rdf:type schema:CreativeWork
    144 https://doi.org/10.1016/j.ic.2006.10.006 schema:sameAs https://app.dimensions.ai/details/publication/pub.1013214343
    145 rdf:type schema:CreativeWork
    146 https://doi.org/10.1016/j.ic.2011.12.003 schema:sameAs https://app.dimensions.ai/details/publication/pub.1038142559
    147 rdf:type schema:CreativeWork
    148 https://doi.org/10.1093/logcom/exn066 schema:sameAs https://app.dimensions.ai/details/publication/pub.1059876216
    149 rdf:type schema:CreativeWork
    150 https://doi.org/10.1109/lics.2002.1029817 schema:sameAs https://app.dimensions.ai/details/publication/pub.1095718758
    151 rdf:type schema:CreativeWork
    152 https://doi.org/10.1109/lics.2010.18 schema:sameAs https://app.dimensions.ai/details/publication/pub.1095349123
    153 rdf:type schema:CreativeWork
    154 https://doi.org/10.1109/lics.2010.24 schema:sameAs https://app.dimensions.ai/details/publication/pub.1095059117
    155 rdf:type schema:CreativeWork
    156 https://doi.org/10.1145/2603088.2603091 schema:sameAs https://app.dimensions.ai/details/publication/pub.1033197618
    157 rdf:type schema:CreativeWork
    158 https://doi.org/10.1145/2603088.2603142 schema:sameAs https://app.dimensions.ai/details/publication/pub.1004660694
    159 rdf:type schema:CreativeWork
    160 https://doi.org/10.1145/360204.375719 schema:sameAs https://app.dimensions.ai/details/publication/pub.1098890971
    161 rdf:type schema:CreativeWork
    162 https://www.grid.ac/institutes/grid.4444.0 schema:alternateName French National Centre for Scientific Research
    163 schema:name LORIA, CNRS, BP 239, 54506, Vandœuvre-lès-Nancy, France
    164 rdf:type schema:Organization
    165 https://www.grid.ac/institutes/grid.462764.5 schema:alternateName Lorraine Research Laboratory in Computer Science and its Applications
    166 schema:name LORIA, Université de Lorraine, BP 239, 54506, Vandœuvre-lès-Nancy, France
    167 rdf:type schema:Organization
    168 https://www.grid.ac/institutes/grid.464035.0 schema:alternateName Laboratoire Spécification et Vérification
    169 schema:name LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, Cachan, France
    170 rdf:type schema:Organization
     




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


    ...