Marcel Kyas will present his work on the project MobiJ and Omega.

In this talk I will present a tool generating proof-outline as PVS theories from a Java class.