WP4: Proof Management

One of the major showstoppers for large programs is that thousands of proof obligations might be generated. Such an amount of proof obligations needs to be handled using an efficient and powerful proof management system.

In addition, whenever automated proof fails, the system has to help the user to understand what failed exactly in term of verification. Therefore traceability between proof obligation, source code and formal specification will be implemented together with a tentative counter-example generation. For advanced users, an interactive proof system for first order logic will be defined.

This work package has an indirect impact on WP1 (Floating-Point Analysis), WP2 (Temporal Properties) and WP3 (Combining Static Analysis Techniques) in the sense that it will help discharging proof obligations created by the analyzers developed in these work packages. Moreover, it will have a direct impact on WP6 (Spreading Static Analysis), since it will tremendously reduce the time and the amount of human work needed to complete the formal verification of properties of large programs.