Graph-based Verification of Reflective Programs

This project will developed new techniques to verify, specify and develop programs with dynamics features, especially reflection, class loading and serialization. To this end it will investigate how dynamic features are used in practice, develop a knowledge-graph based library for development and specification, and finally develop a deductive verification tool to verify Java programs against such specifications.