Personal tools

Falsifying Analyses

From PUMA Graduiertenkolleg

Revision as of 13:02, 25 October 2010 by Seidl (talk | contribs) (Summary)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Summary

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.

Topics