ABSTRACT:
We give an overview over various techniques used for the automatic
verification of systems with infinitely many different reachable states.
Infinite state-spaces are due to features like unbounded recursion,
parallel process creation, counters, clocks, buffers for asynchronous
communication, and unbounded data types. In particular, we focus on the
field of semantic equivalence checking and present an abstract result that
explains why simulation checking is computationally harder than
bisimulation checking.  Furthermore, we report on some work on applied
verification and the IBOC-tool.  This tool implements a scalable method
for automatically checking buffer-overflow conditions in UML RT and
Promela models. Finally, we describe the results of some case studies with
IBOC.