@MastersThesis{Dyck2012,
AUTHOR = {Dyck, Johannes},
TITLE = {{Increasing expressive power of graph rules and conditions and automatic verification with inductive invariants}},
YEAR = {2012},
MONTH = {July},
SCHOOL = {Hasso-Plattner-Institut für Softwaresystemtechnik, Universität Potsdam},
OPTacc_ABSTRACT = {Invariant checking in general and inductive invariants in particular are static analysis techniques in the field of model checking. Based on an existing tool concerned with the verification of inductive invariants using graph transformation sys- tems, we present a number of extensions to enhance the functionality and applicability of the tool. Since the usefulness of our tool is in direct relation to its expressiveness when describing systems, we aim to increase the expressive power of our specification language employed to formulate graph rules and invariants. To ensure the correctness of our approach we relate our technique to the underlying theoretical foundations of graph transformations and give proof. Finally, we introduce a configuration language to improve both the flexibility and applicability of our tool and the reusability of our components. }
}