June 06, 2013Presentation: Algorithm Refinement using Dynamic Logic
Room: Zi 2126Mattias Ulbrich

This thesis is concerned with the deductive verification of Java programs with respect to a full functional specification.

Two successful ideas in deductive program verification are combined in a new and flexible approach: Deductive verification using dynamic logic is brought together with an intermediate verification language. This language is general enough to serve as target language for verification conditions from many input languages, for instance Java bytecode or pseudocode.

Approaches in formal software verification have mostly been either purely abstract or purely on an implementational level, the relationship between the levels has seldom been subject of investigation.

This thesis builds a bridge between the two worlds of verification by applying the well-established instrument of refinement which is an established technique in model verification. It has, however, seldom been applied to a refinement from abstract descriptions to actual program source code. The thesis describes a methodology to write algorithms in a purely abstract, mathematical pseudocode language which are then refined to actually executable code in Java. This allows a canonical separation of verification concerns: Interesting functional properties can be defined, examined and verified on the algorithmic level where implementational details can be kept aside. The formal refinement then transfers the verification results into results on the implementation level without that proofs needed to be conducted a second time on that level. The dynamic logic and the intermediate language are important building blocks of the methodology.