@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{GabrysiakGieseSeibel2011,
  author    = {Gabrysiak, Gregor and Giese, Holger and Seibel, Andreas},
  title     = {Towards next generation design thinking : scenario-based prototyping for designing complex software systems with multiple users},
  isbn      = {978-3-642-13756-3},
  year      = {2011},
  language  = {en}
}
@article{GabrysiakGieseSeibel2012,
  author    = {Gabrysiak, Gregor and Giese, Holger and Seibel, Andreas},
  title     = {Towards next-generation design thinking II : virtual muti-user software prototypes},
  year      = {2012},
  language  = {en}
}
@article{BandyopadhyaySarkarMandaletal.2022,
  author    = {Bandyopadhyay, Soumyadip and Sarkar, Dipankar and Mandal, Chittaranjan and Giese, Holger},
  title     = {Translation validation of coloured Petri net models of programs on integers},
  series = {Acta informatica},
  volume    = {59},
  journal   = {Acta informatica},
  number    = {6},
  publisher = {Springer},
  address   = {New York},
  issn      = {0001-5903},
  doi       = {10.1007/s00236-022-00419-z},
  pages     = {725 -- 759},
  year      = {2022},
  abstract  = {Programs are often subjected to significant optimizing and parallelizing transformations based on extensive dependence analysis. Formal validation of such transformations needs modelling paradigms which can capture both control and data dependences in the program vividly. Being value-based with an inherent scope of capturing parallelism, the untimed coloured Petri net (CPN) models, reported in the literature, fit the bill well; accordingly, they are likely to be more convenient as the intermediate representations (IRs) of both the source and the transformed codes for translation validation than strictly sequential variable-based IRs like sequential control flow graphs (CFGs). In this work, an efficient path-based equivalence checking method for CPN models of programs on integers is presented. Extensive experimentation has been carried out on several sequential and parallel examples. Complexity and correctness issues have been treated rigorously for the method.},
  language  = {en}
}