During this talk I will give an overview of the contents of my Masters thesis, which is about implementing a translation of annotated Java to HOL-syntax using ASF+SDF. ASF+SDF is a formalism that is useful for rapid specification of syntax transformations, while HOL is the theorem prover used to verify the output of the tool written in ASF+SDF.

The emphasis will be on the theory used, which is based on flowcharts, but the talk will be concluded with an example that has been verified using this tool.