@book{DyckGiese2017,
  author    = {Dyck, Johannes and Giese, Holger},
  title     = {k-Inductive invariant checking for graph transformation systems},
  number    = {119},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-406-7},
  issn      = {1613-5652},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-397044},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {45},
  year      = {2017},
  abstract  = {While offering significant expressive power, graph transformation systems often come with rather limited capabilities for automated analysis, particularly if systems with many possible initial graphs and large or infinite state spaces are concerned. One approach that tries to overcome these limitations is inductive invariant checking. However, the verification of inductive invariants often requires extensive knowledge about the system in question and faces the approach-inherent challenges of locality and lack of context. To address that, this report discusses k-inductive invariant checking for graph transformation systems as a generalization of inductive invariants. The additional context acquired by taking multiple (k) steps into account is the key difference to inductive invariant checking and is often enough to establish the desired invariants without requiring the iterative development of additional properties. To analyze possibly infinite systems in a finite fashion, we introduce a symbolic encoding for transformation traces using a restricted form of nested application conditions. As its central contribution, this report then presents a formal approach and algorithm to verify graph constraints as k-inductive invariants. We prove the approach's correctness and demonstrate its applicability by means of several examples evaluated with a prototypical implementation of our algorithm.},
  language  = {en}
}
@book{DyckGiese2015,
  author    = {Dyck, Johannes and Giese, Holger},
  title     = {Inductive invariant checking with partial negative application conditions},
  number    = {98},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-333-6},
  issn      = {1613-5652},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-77748},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {43},
  year      = {2015},
  abstract  = {Graph transformation systems are a powerful formal model to capture model transformations or systems with infinite state space, among others. However, this expressive power comes at the cost of rather limited automated analysis capabilities. The general case of unbounded many initial graphs or infinite state spaces is only supported by approaches with rather limited scalability or expressiveness. In this report we improve an existing approach for the automated verification of inductive invariants for graph transformation systems. By employing partial negative application conditions to represent and check many alternative conditions in a more compact manner, we can check examples with rules and constraints of substantially higher complexity. We also substantially extend the expressive power by supporting more complex negative application conditions and provide higher accuracy by employing advanced implication checks. The improvements are evaluated and compared with another applicable tool by considering three case studies.},
  language  = {en}
}