The project ist concerned with new methods for automated software verification, in particular by model checking, testing, and abstract interpretation. The project has a focus on heuristics to exploit informal information from the program in the analysis.