@article{SchneiderLambersOrejas2018,
  author    = {Schneider, Sven and Lambers, Leen and Orejas, Fernando},
  title     = {Automated reasoning for attributed graph properties},
  series = {International Journal on Software Tools for Technology Transfer},
  volume    = {20},
  journal   = {International Journal on Software Tools for Technology Transfer},
  number    = {6},
  publisher = {Springer},
  address   = {Heidelberg},
  issn      = {1433-2779},
  doi       = {10.1007/s10009-018-0496-3},
  pages     = {705 -- 737},
  year      = {2018},
  abstract  = {Graphs are ubiquitous in computer science. Moreover, in various application fields, graphs are equipped with attributes to express additional information such as names of entities or weights of relationships. Due to the pervasiveness of attributed graphs, it is highly important to have the means to express properties on attributed graphs to strengthen modeling capabilities and to enable analysis. Firstly, we introduce a new logic of attributed graph properties, where the graph part and attribution part are neatly separated. The graph part is equivalent to first-order logic on graphs as introduced by Courcelle. It employs graph morphisms to allow the specification of complex graph patterns. The attribution part is added to this graph part by reverting to the symbolic approach to graph attribution, where attributes are represented symbolically by variables whose possible values are specified by a set of constraints making use of algebraic specifications. Secondly, we extend our refutationally complete tableau-based reasoning method as well as our symbolic model generation approach for graph properties to attributed graph properties. Due to the new logic mentioned above, neatly separating the graph and attribution parts, and the categorical constructions employed only on a more abstract level, we can leave the graph part of the algorithms seemingly unchanged. For the integration of the attribution part into the algorithms, we use an oracle, allowing for flexible adoption of different available SMT solvers in the actual implementation. Finally, our automated reasoning approach for attributed graph properties is implemented in the tool AutoGraph integrating in particular the SMT solver Z3 for the attribute part of the properties. We motivate and illustrate our work with a particular application scenario on graph database query validation.},
  language  = {en}
}
@article{SchneiderLambersOrejas2021,
  author    = {Schneider, Sven and Lambers, Leen and Orejas, Fernando},
  title     = {A logic-based incremental approach to graph repair featuring delta preservation},
  series = {International journal on software tools for technology transfer : STTT},
  volume    = {23},
  journal   = {International journal on software tools for technology transfer : STTT},
  number    = {3},
  publisher = {Springer},
  address   = {Berlin ; Heidelberg},
  issn      = {1433-2779},
  doi       = {10.1007/s10009-020-00584-x},
  pages     = {369 -- 410},
  year      = {2021},
  abstract  = {We introduce a logic-based incremental approach to graph repair, generating a sound and complete (upon termination) overview of least-changing graph repairs from which a user may select a graph repair based on non-formalized further requirements. This incremental approach features delta preservation as it allows to restrict the generation of graph repairs to delta-preserving graph repairs, which do not revert the additions and deletions of the most recent consistency-violating graph update. We specify consistency of graphs using the logic of nested graph conditions, which is equivalent to first-order logic on graphs. Technically, the incremental approach encodes if and how the graph under repair satisfies a graph condition using the novel data structure of satisfaction trees, which are adapted incrementally according to the graph updates applied. In addition to the incremental approach, we also present two state-based graph repair algorithms, which restore consistency of a graph independent of the most recent graph update and which generate additional graph repairs using a global perspective on the graph under repair. We evaluate the developed algorithms using our prototypical implementation in the tool AutoGraph and illustrate our incremental approach using a case study from the graph database domain.},
  language  = {en}
}
@book{SchneiderLambersOrejas2017,
  author    = {Schneider, Sven and Lambers, Leen and Orejas, Fernando},
  title     = {Symbolic model generation for graph properties},
  number    = {115},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-396-1},
  issn      = {1613-5652},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-103171},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {48},
  year      = {2017},
  abstract  = {Graphs are ubiquitous in Computer Science. For this reason, in many areas, it is very important to have the means to express and reason about graph properties. In particular, we want to be able to check automatically if a given graph property is satisfiable. Actually, in most application scenarios it is desirable to be able to explore graphs satisfying the graph property if they exist or even to get a complete and compact overview of the graphs satisfying the graph property. We show that the tableau-based reasoning method for graph properties as introduced by Lambers and Orejas paves the way for a symbolic model generation algorithm for graph properties. Graph properties are formulated in a dedicated logic making use of graphs and graph morphisms, which is equivalent to firstorder logic on graphs as introduced by Courcelle. Our parallelizable algorithm gradually generates a finite set of so-called symbolic models, where each symbolic model describes a set of finite graphs (i.e., finite models) satisfying the graph property. The set of symbolic models jointly describes all finite models for the graph property (complete) and does not describe any finite graph violating the graph property (sound). Moreover, no symbolic model is already covered by another one (compact). Finally, the algorithm is able to generate from each symbolic model a minimal finite model immediately and allows for an exploration of further finite models. The algorithm is implemented in the new tool AutoGraph.},
  language  = {en}
}
@book{SchneiderLambersOrejas2019,
  author    = {Schneider, Sven and Lambers, Leen and Orejas, Fernando},
  title     = {A logic-based incremental approach to graph repair},
  number    = {126},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-462-3},
  issn      = {1613-5652},
  doi       = {10.25932/publishup-42751},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-427517},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {34},
  year      = {2019},
  abstract  = {Graph repair, restoring consistency of a graph, plays a prominent role in several areas of computer science and beyond: For example, in model-driven engineering, the abstract syntax of models is usually encoded using graphs. Flexible edit operations temporarily create inconsistent graphs not representing a valid model, thus requiring graph repair. Similarly, in graph databases—managing the storage and manipulation of graph data—updates may cause that a given database does not satisfy some integrity constraints, requiring also graph repair. We present a logic-based incremental approach to graph repair, generating a sound and complete (upon termination) overview of least-changing repairs. In our context, we formalize consistency by so-called graph conditions being equivalent to first-order logic on graphs. We present two kind of repair algorithms: State-based repair restores consistency independent of the graph update history, whereas deltabased (or incremental) repair takes this history explicitly into account. Technically, our algorithms rely on an existing model generation algorithm for graph conditions implemented in AutoGraph. Moreover, the delta-based approach uses the new concept of satisfaction (ST) trees for encoding if and how a graph satisfies a graph condition. We then demonstrate how to manipulate these STs incrementally with respect to a graph update.},
  language  = {en}
}