From PUMA Graduiertenkolleg
The correctness of an assertion such as that a program satisfies a specification can only be proven if the assertion is definitively true. In order to reduce the overhead of failing proof attempts, techniques are required which quickly exhibit wrong assumptions.
Beyond that, uncovering run-time errors in systems at an early stage of program development significantly improves and accelerates the software development process.
The goal is to find new applications for model-checking, abstract interpretation and theorem proving or their combinations in the area of falsification of assertions from more general system descriptions and more powerful logics and also to enhance precision and coverage significantly.