Using ASF+SDF for the Verification of Annotated Java Programs

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.  

hosted by