SMT-based Flat Model-Checking for LTL with Counting

In this thesis a new approach for underapproximation-based modelchecking is implemented. It relies on theoretical results in model-checking of temporal logics with counting capabilities over flat structures. The developed method uses the concept of path schemas to encode program runs which contain multiple loops compactly. Applied to general counter systems this yields a new approach that generalizes bounded model-checking in a way that in certain circumstances enables the calculation of counterexamples which otherwise would not be practically obtainable. After a formal introduction of all concepts the logic lcLTL is defined and proposed as a specification language. Then a translation of the existential model-checking problem for this logic into a satisfiability problem of quantifier-free Presburger arithmetic is described and finally a prototype implementation is discussed and evaluated on a selection of examples.