@article{DyckGieseLambers2019,
  author    = {Dyck, Johannes and Giese, Holger and Lambers, Leen},
  title     = {Automatic verification of behavior preservation at the transformation level for relational model transformation},
  series = {Software and systems modeling},
  volume    = {18},
  journal   = {Software and systems modeling},
  number    = {5},
  publisher = {Springer},
  address   = {Heidelberg},
  issn      = {1619-1366},
  doi       = {10.1007/s10270-018-00706-9},
  pages     = {2937 -- 2972},
  year      = {2019},
  abstract  = {The correctness of model transformations is a crucial element for model-driven engineering of high-quality software. In particular, behavior preservation is an important correctness property avoiding the introduction of semantic errors during the model-driven engineering process. Behavior preservation verification techniques show some kind of behavioral equivalence or refinement between source and target model of the transformation. Automatic tool support is available for verifying behavior preservation at the instance level, i.e., for a given source and target model specified by the model transformation. However, until now there is no sound and automatic verification approach available at the transformation level, i.e., for all source and target models. In this article, we extend our results presented in earlier work (Giese and Lambers, in: Ehrig et al (eds) Graph transformations, Springer, Berlin, 2012) and outline a new transformation-level approach for the sound and automatic verification of behavior preservation captured by bisimulation resp.simulation for outplace model transformations specified by triple graph grammars and semantic definitions given by graph transformation rules. In particular, we first show how behavior preservation can be modeled in a symbolic manner at the transformation level and then describe that transformation-level verification of behavior preservation can be reduced to invariant checking of suitable conditions for graph transformations. We demonstrate that the resulting checking problem can be addressed by our own invariant checker for an example of a transformation between sequence charts and communicating automata.},
  language  = {en}
}
@article{OrejasPinoNavarroetal.2018,
  author    = {Orejas, Fernando and Pino, Elvira and Navarro, Marisa and Lambers, Leen},
  title     = {Institutions for navigational logics for graphical structures},
  series = {Theoretical computer science},
  volume    = {741},
  journal   = {Theoretical computer science},
  publisher = {Elsevier},
  address   = {Amsterdam},
  issn      = {0304-3975},
  doi       = {10.1016/j.tcs.2018.02.031},
  pages     = {19 -- 24},
  year      = {2018},
  abstract  = {We show that a Navigational Logic, i.e., a logic to express properties about graphs and about paths in graphs is a semi-exact institution. In this way, we can use a number of operations to structure and modularize our specifications. Moreover, using the properties of our institution, we also show how to structure single formulas, which in our formalism could be quite complex.},
  language  = {en}
}
@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{LambersBornKosioletal.2018,
  author    = {Lambers, Leen and Born, Kristopher and Kosiol, Jens and Str{\"u}ber, Daniel and Taentzer, Gabriele},
  title     = {Granularity of conflicts and dependencies in graph transformation systems},
  series = {Journal of Logical and Algebraic Methods in Programming},
  volume    = {103},
  journal   = {Journal of Logical and Algebraic Methods in Programming},
  publisher = {Elsevier},
  address   = {New York},
  issn      = {2352-2208},
  doi       = {10.1016/j.jlamp.2018.11.004},
  pages     = {105 -- 129},
  year      = {2018},
  abstract  = {Conflict and dependency analysis (CDA) is a static analysis for the detection of conflicting and dependent rule applications in a graph transformation system. The state-of-the-art CDA technique, critical pair analysis, provides all potential conflicts and dependencies in minimal context as critical pairs, for each pair of rules. Yet, critical pairs can be hard to understand; users are mainly interested in core information about conflicts and dependencies occurring in various combinations. In this paper, we present an approach to conflicts and dependencies in graph transformation systems based on two dimensions of granularity. The first dimension refers to the overlap considered between the rules of a given rule pair; the second one refers to the represented amount of context information about transformations in which the conflicts occur. We introduce a variety of new conflict notions, in particular, conflict atoms, conflict reasons, and minimal conflict reasons, relate them to the existing conflict notions of critical pairs and initial conflicts, and position all of these notions within our granularity approach. Finally, we introduce dual concepts for dependency analysis. As we discuss in a running example, our approach paves the way for an improved CDA technique. (C) 2018 Elsevier Inc. All rights reserved.},
  language  = {en}
}
@article{LambersWeber2020,
  author    = {Lambers, Leen and Weber, Jens},
  title     = {Preface to the special issue on the 11th International Conference on Graph Transformation},
  series = {Journal of Logical and Algebraic Methods in Programming},
  volume    = {112},
  journal   = {Journal of Logical and Algebraic Methods in Programming},
  publisher = {Elsevier},
  address   = {Amsterdam},
  issn      = {2352-2208},
  doi       = {10.1016/j.jlamp.2020.100525},
  pages     = {2},
  year      = {2020},
  abstract  = {This special issue contains extended versions of four selected papers from the 11th International Conference on Graph Transformation (ICGT 2018). The articles cover a tool for computing core graphs via SAT/SMT solvers (graph language definition), graph transformation through graph surfing in reaction systems (a new graph transformation formalism), the essence and initiality of conflicts in M-adhesive transformation systems, and a calculus of concurrent graph-rewriting processes (theory on conflicts and parallel independence).},
  language  = {en}
}
@article{GolasLambersEhrigetal.2012,
  author    = {Golas, Ulrike and Lambers, Leen and Ehrig, Hartmut and Orejas, Fernando},
  title     = {Attributed graph transformation with inheritance: Efficient conflict detection and local confluence analysis using abstract critical pairs},
  series = {THEORETICAL COMPUTER SCIENCE},
  volume    = {424},
  journal   = {THEORETICAL COMPUTER SCIENCE},
  publisher = {ELSEVIER SCIENCE BV},
  address   = {AMSTERDAM},
  issn      = {0304-3975},
  doi       = {10.1016/j.tcs.2012.01.032},
  pages     = {46 -- 68},
  year      = {2012},
  abstract  = {Inheritance is an important and widely spread concept enabling the elegant expression of hierarchy in object-oriented software programs or models. It has been defined for graphs and graph transformations enhancing the applicability of this formal technique. Up to now, for the analysis of transformations with inheritance a flattening construction has been used, which yields all the well-known results for graph transformation but results in a large number of graphs and rules that have to be analyzed. In this paper, we introduce a new category of typed attributed graphs with inheritance. For the detection of conflicts between graph transformations on these graphs, the notion of abstract critical pairs is defined. This allows us to perform the analysis on polymorphic rules and transformations without the need for flattening, which significantly increases the efficiency of the analysis and eases the interpretation of the analysis results. The new main result is the Local Confluence Theorem for typed attributed graph transformation with inheritance using abstract critical pairs. All constructions and results are demonstrated on an example for the analysis of refactorings. (C) 2012 Elsevier B.V. All rights reserved.},
  language  = {en}
}
@article{GieseHildebrandtLambers2014,
  author    = {Giese, Holger and Hildebrandt, Stephan and Lambers, Leen},
  title     = {Bridging the gap between formal semantics and implementation of triple graph grammars},
  series = {Software and systems modeling},
  volume    = {13},
  journal   = {Software and systems modeling},
  number    = {1},
  publisher = {Springer},
  address   = {Heidelberg},
  issn      = {1619-1366},
  doi       = {10.1007/s10270-012-0247-y},
  pages     = {273 -- 299},
  year      = {2014},
  abstract  = {The correctness of model transformations is a crucial element for model-driven engineering of high-quality software. A prerequisite to verify model transformations at the level of the model transformation specification is that an unambiguous formal semantics exists and that the implementation of the model transformation language adheres to this semantics. However, for existing relational model transformation approaches, it is usually not really clear under which constraints particular implementations really conform to the formal semantics. In this paper, we will bridge this gap for the formal semantics of triple graph grammars (TGG) and an existing efficient implementation. While the formal semantics assumes backtracking and ignores non-determinism, practical implementations do not support backtracking, require rule sets that ensure determinism, and include further optimizations. Therefore, we capture how the considered TGG implementation realizes the transformation by means of operational rules, define required criteria, and show conformance to the formal semantics if these criteria are fulfilled. We further outline how static and runtime checks can be employed to guarantee these criteria.},
  language  = {en}
}
@article{EhrigGolasHabeletal.2012,
  author    = {Ehrig, Hartmut and Golas, Ulrike and Habel, Annegret and Lambers, Leen and Orejas, Fernando},
  title     = {M-Adhesive Transformation Systems with Nested Application Conditions Part 2: Embedding, Critical Pairs and Local Confluence},
  series = {Fundamenta informaticae},
  volume    = {118},
  journal   = {Fundamenta informaticae},
  number    = {1-2},
  publisher = {IOS Press},
  address   = {Amsterdam},
  issn      = {0169-2968},
  doi       = {10.3233/FI-2012-705},
  pages     = {35 -- 63},
  year      = {2012},
  abstract  = {Graph transformation systems have been studied extensively and applied to several areas of computer science like formal language theory, the modeling of databases, concurrent or distributed systems, and visual, logical, and functional programming. In most kinds of applications it is necessary to have the possibility of restricting the applicability of rules. This is usually done by means of application conditions. In this paper, we continue the work of extending the fundamental theory of graph transformation to the case where rules may use arbitrary (nested) application conditions. More precisely, we generalize the Embedding theorem, and we study how local confluence can be checked in this context. In particular, we define a new notion of critical pair which allows us to formulate and prove a Local Confluence Theorem for the general case of rules with nested application conditions. All our results are presented, not for a specific class of graphs, but for any arbitrary M-adhesive category, which means that our results apply to most kinds of graphical structures. We demonstrate our theory on the modeling of an elevator control by a typed graph transformation system with positive and negative application conditions.},
  language  = {en}
}
@article{OrejasLambers2012,
  author    = {Orejas, Fernando and Lambers, Leen},
  title     = {Lazy graph transformation},
  series = {Fundamenta informaticae},
  volume    = {118},
  journal   = {Fundamenta informaticae},
  number    = {1-2},
  publisher = {IOS Press},
  address   = {Amsterdam},
  issn      = {0169-2968},
  doi       = {10.3233/FI-2012-706},
  pages     = {65 -- 96},
  year      = {2012},
  abstract  = {Applying an attributed graph transformation rule to a given object graph always implies some kind of constraint solving. In many cases, the given constraints are almost trivial to solve. For instance, this is the case when a rule describes a transformation G double right arrow H, where the attributes of H are obtained by some simple computation from the attributes of G. However there are many other cases where the constraints to solve may be not so trivial and, moreover, may have several answers. This is the case, for instance, when the transformation process includes some kind of searching. In the current approaches to attributed graph transformation these constraints must be completely solved when defining the matching of the given transformation rule. This kind of early binding is well-known from other areas of Computer Science to be inadequate. For instance, the solution chosen for the constraints associated to a given transformation step may be not fully adequate, meaning that later, in the search for a better solution, we may need to backtrack this transformation step. In this paper, based on our previous work on the use of symbolic graphs to deal with different aspects related with attributed graphs, including attributed graph transformation, we present a new approach that, based on the new notion of narrowing graph transformation rule, allows us to delay constraint solving when doing attributed graph transformation, in a way that resembles lazy computation. For this reason, we have called lazy this new kind of transformation. Moreover, we show that the approach is sound and complete with respect to standard attributed graph transformation. A running example, where a graph transformation system describes some basic operations of a travel agency, shows the practical interest of the approach.},
  language  = {en}
}
@article{EhrigGolasHabeletal.2014,
  author    = {Ehrig, Hartmut and Golas, Ulrike and Habel, Annegret and Lambers, Leen and Orejas, Fernando},
  title     = {M-adhesive transformation systems with nested application conditions. Part 1: parallelism, concurrency and amalgamation},
  series = {Mathematical structures in computer science : a journal in the applications of categorical, algebraic and geometric methods in computer science},
  volume    = {24},
  journal   = {Mathematical structures in computer science : a journal in the applications of categorical, algebraic and geometric methods in computer science},
  number    = {4},
  publisher = {Cambridge Univ. Press},
  address   = {New York},
  issn      = {0960-1295},
  doi       = {10.1017/S0960129512000357},
  pages     = {48},
  year      = {2014},
  abstract  = {Nested application conditions generalise the well-known negative application conditions and are important for several application domains. In this paper, we present Local Church-Rosser, Parallelism, Concurrency and Amalgamation Theorems for rules with nested application conditions in the framework of M-adhesive categories, where M-adhesive categories are slightly more general than weak adhesive high-level replacement categories. Most of the proofs are based on the corresponding statements for rules without application conditions and two shift lemmas stating that nested application conditions can be shifted over morphisms and rules.},
  language  = {en}
}