Sep 28, 2015
Hiroshi Unno: Verification of Featherweight Java Programs via Transformation to Higher-order Functional Programs with Recursive Data Types
In this talk, I will present a verification method for object-oriented programs in Featherweight Java (FJ) based on a transformation to functional programs in ML. The transformation encodes objects and dynamic method dispatching in FJ using higher-order functions and recursive data types in ML. The transformed programs are then verified by using the state-of-the-art techniques for ML programs such as refinement types, Horn clause solving, and higher-order model checking. In the talk, I will explain one of the techniques called refinement type optimization which we have proposed in SAS 2015.