Presentation: Source-code based formal techniques for fault-detection, testing, and specification of Java programs.

When: April 9, 2015, 11:30-12:30

Where: ZI2042

Who: Christoph Gladisch

This talk presents a set of formal techniques for detecting faults in single-threaded Java programs, for generating test cases, and for writing specifications. Most of the techniques are based on the deductive verification tool KeY and focus on the analysis of individual methods on the source code level. The talk provides an overview of different contributions and explains the key ideas of several techniques.